metamath

Messages by Date

2023/07/14 Re: [Metamath] Metamath-lamp version 14 released, now with undo David A. Wheeler
2023/07/14 [Metamath] Reminder: We still have Metamath 100 entries to complete!! David A. Wheeler
2023/07/14 [Metamath] Metamath-lamp version 14 released, now with undo David A. Wheeler
2023/07/13 AW: [Metamath] The Math Genome Project - feedback request Discher, Samiro
2023/07/13 [Metamath] The Math Genome Project - feedback request Johnathan Mercer
2023/07/12 AW: [Metamath] Uncomfortable with definitions as axioms ... help? Discher, Samiro
2023/07/12 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/12 AW: [Metamath] Uncomfortable with definitions as axioms ... help? Discher, Samiro
2023/07/12 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Mario Carneiro
2023/07/12 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/11 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/11 AW: [Metamath] Uncomfortable with definitions as axioms ... help? Discher, Samiro
2023/07/11 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Mario Carneiro
2023/07/11 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/11 [Metamath] Re: How do you quickly jump to the markup definitions in set.mm? Marshall Stoner
2023/07/09 [Metamath] How do you quickly jump to the markup definitions in set.mm? Marshall Stoner
2023/07/09 [Metamath] Metamath-lamp version 13 released David Wheeler
2023/07/08 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/08 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Marshall Stoner
2023/07/06 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
2023/07/04 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
2023/07/04 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
2023/07/04 Re: [Metamath] I cannot open mmj2: mmj.pa.MMJException: E-UT-1502 Error Mázsa Péter
2023/07/04 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
2023/07/04 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
2023/07/04 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. David A. Wheeler
2023/07/03 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
2023/07/03 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
2023/07/03 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
2023/07/03 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
2023/07/03 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
2023/07/03 [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
2023/06/29 [Metamath] Metamath is famous! Tau Day famous that is Jim Kingdon
2023/06/27 Re: [Metamath] Video of "Introduction to Metamath-lamp, part 3" David A. Wheeler
2023/06/26 [Metamath] Metamath-lamp version 11 has been released! David A. Wheeler
2023/06/25 [Metamath] Re: Video of "Introduction to Metamath-lamp, part 3" Igor Ieskov
2023/06/25 [Metamath] Video of "Introduction to Metamath-lamp, part 3" David Wheeler
2023/06/25 [Metamath] Updated video of "Introduction to Metamath-lamp, part 2" David A . Wheeler
2023/06/24 Re: [Metamath] Metamath-lamp video, part 1 Jim Kingdon
2023/06/24 [Metamath] Draft Metamath-lamp video, part **2** David A. Wheeler
2023/06/24 [Metamath] Metamath-lamp video, part 1 David A. Wheeler
2023/06/17 [Metamath] Metamath website page updates continue David A. Wheeler
2023/06/11 Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
2023/06/11 [Metamath] Re: Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
2023/06/11 [Metamath] Re: Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
2023/06/11 [Metamath] Is there a way to show all mandatory hypotheses of a statement on the Metamath program? Humanities Clinic
2023/06/10 Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
2023/06/09 [Metamath] Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
2023/06/08 [Metamath] kids these days Jim Kingdon
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Mario Carneiro
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Thierry Arnoux
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Mario Carneiro
2023/06/08 Re: [Metamath] How are typecodes used/enforced by the Metamath program? David A. Wheeler
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? David A. Wheeler
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Igor Ieskov
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/08 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/07 Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it Paul Chapman
2023/06/07 Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it Jim Kingdon
2023/06/07 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/07 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/07 [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
2023/06/06 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/06 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Thierry Arnoux
2023/06/06 Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Thierry Arnoux
2023/06/06 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/06 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? David A. Wheeler
2023/06/06 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/05 Re: [Metamath] How are typecodes used/enforced by the Metamath program? Mario Carneiro
2023/06/05 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/05 [Metamath] Re: How are typecodes used/enforced by the Metamath program? Humanities Clinic
2023/06/05 Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Jim Kingdon
2023/06/05 Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
2023/06/05 Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? David A. Wheeler
2023/06/05 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/05 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/04 [Metamath] How are typecodes used/enforced by the Metamath program? Humanities Clinic
2023/06/04 Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
2023/06/04 AW: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Discher, Samiro
2023/06/04 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? David A. Wheeler
2023/06/04 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? David A. Wheeler
2023/06/04 Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Thierry Arnoux
2023/06/04 [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
2023/06/04 [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset? Humanities Clinic
2023/06/04 [Metamath] Re: Yamma Glauco
2023/06/01 Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Thierry Arnoux
2023/05/31 Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Jim Kingdon
2023/05/31 Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Mario Carneiro
2023/05/31 [Metamath] How to Understand The "More Complicated" Expressions in Definitions Humanities Clinic
2023/05/30 [Metamath] "Metamath-lamp Guide" now visible at: https://lamp-guide.metamath.org/ David A. Wheeler
2023/05/29 Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Jim Kingdon
2023/05/29 [Metamath] Re: I intend to create a new metamath org repository named "lamp-guide" David A. Wheeler
2023/05/29 [Metamath] I intend to create a new metamath org repository named "lamp-guide" David A. Wheeler
2023/05/29 Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Mario Carneiro
2023/05/29 [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Humanities Clinic
2023/05/28 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) Mario Carneiro
2023/05/28 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) Igor Ieskov
2023/05/28 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) 'Alexander van der Vekens' via Metamath
2023/05/27 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) Igor Ieskov
2023/05/27 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) David A. Wheeler
2023/05/27 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) 'Alexander van der Vekens' via Metamath
2023/05/26 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) David A. Wheeler
2023/05/26 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) 'Alexander van der Vekens' via Metamath
2023/05/26 Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) Thierry Arnoux
2023/05/23 [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least) David A. Wheeler
2023/05/12 Re: [Metamath] eqsb3lem vs eqsb3v 'Alexander van der Vekens' via Metamath
2023/05/11 Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs Jon P
2023/05/09 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/05/09 Re: [Metamath] Web-based mmj2-like proof assistant David Starner
2023/05/09 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/05/08 Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
2023/05/07 Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
2023/05/07 Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs Jon P
2023/05/06 [Metamath] Re: An exhaustive generator for the mmsolitaire project Samiro Discher
2023/05/04 Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
2023/05/03 Re: [Metamath] eqsb3lem vs eqsb3v Zheng Fan
2023/05/02 Re: [Metamath] eqsb3lem vs eqsb3v David A. Wheeler
2023/05/02 [Metamath] eqsb3lem vs eqsb3v Zheng Fan
2023/04/30 Re: [Metamath] Yamma Glauco
2023/04/27 Re: [Metamath] Yamma Glauco
2023/04/27 Re: [Metamath] Yamma Thierry Arnoux
2023/04/26 Re: [Metamath] Yamma Glauco
2023/04/26 Re: [Metamath] Yamma Thierry Arnoux
2023/04/24 Re: [Metamath] OpenAI Proof Assistant for Metamath Aleksandras Maliuginas
2023/04/24 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/04/19 Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d LM
2023/04/19 Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d Mario Carneiro
2023/04/19 Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d Mario Carneiro
2023/04/19 Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Jim Kingdon
2023/04/19 Re: [Metamath] mmj2 Export GMMF LM
2023/04/19 Re: [Metamath] mmj2 Export GMMF LM
2023/04/19 Re: [Metamath] mmj2 Export GMMF Mázsa Péter
2023/04/19 [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d LM
2023/04/19 [Metamath] mmj2 Export GMMF LM
2023/04/19 Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) LM
2023/04/19 Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Igor Ieskov
2023/04/18 Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Mario Carneiro
2023/04/18 [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) LM
2023/04/17 Re: [Metamath] Re: My contribution to Metamath's mmsolitaire project Samiro Discher
2023/04/17 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Antony Bartlett
2023/04/17 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Paul Chapman
2023/04/17 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Glauco
2023/04/16 Re: [Metamath] Re: Formalizing Fermat's Last Theorem LM
2023/04/10 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/04/05 [Metamath] Re: Reverse polish notation proofs from first principles exclusively Samiro Discher
2023/04/05 [Metamath] Re: Reverse polish notation proofs from first principles exclusively Samiro Discher
2023/04/05 Re: [Metamath] Reverse polish notation proofs from first principles exclusively Mario Carneiro
2023/04/05 [Metamath] Reverse polish notation proofs from first principles exclusively Guram Mikaberidze
2023/04/03 Re: [Metamath] Re: mmj2 compact representation for $d statements Glauco
2023/04/03 Re: [Metamath] Re: mmj2 compact representation for $d statements Glauco
2023/04/02 Re: [Metamath] Re: mmj2 compact representation for $d statements Mario Carneiro
2023/04/02 Re: [Metamath] Re: mmj2 compact representation for $d statements Mario Carneiro
2023/04/02 [Metamath] Re: mmj2 compact representation for $d statements Benoit
2023/04/02 [Metamath] mmj2 compact representation for $d statements Glauco
2023/03/31 [Metamath] Re: Speculations on how to help machine learning systems generate metamath proofs Jon P
2023/03/25 [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
2023/03/17 [Metamath] Re: Negative use cases database? Glauco
2023/03/16 Re: [Metamath] Negative use cases database? Jim Kingdon
2023/03/11 [Metamath] Re: Metamath website - current status Samiro Discher
2023/03/10 Re: [Metamath] mmj2 error js does not exist David A. Wheeler
2023/03/10 Re: [Metamath] Negative use cases database? Mario Carneiro
2023/03/10 Re: [Metamath] Metamatix Mario Carneiro
2023/03/10 [Metamath] Negative use cases database? Samuel Goto
2023/03/10 Re: [Metamath] Metamatix Denis Carnier
2023/03/06 Re: [Metamath] mmj2 error js does not exist jannik vierling
2023/03/05 Re: [Metamath] mmj2 error js does not exist David A. Wheeler
2023/03/05 Re: [Metamath] mmj2 error js does not exist Benoit
2023/03/04 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/04 Re: [Metamath] mmj2 error js does not exist jannik vierling
2023/03/04 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/04 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/04 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist David Crisp
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/03 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/03 Re: [Metamath] mmj2 error js does not exist David Crisp
2023/03/02 Re: [Metamath] Future website directions Mario Carneiro
2023/03/02 Re: [Metamath] mmj2 error js does not exist David A. Wheeler
2023/03/02 Re: [Metamath] Future website directions David A. Wheeler
2023/03/02 [Metamath] Re: Metamath website - current status Glauco
2023/03/02 Re: [Metamath] mmj2 error js does not exist Mario Carneiro
2023/03/02 Re: [Metamath] Future website directions Mario Carneiro
2023/03/02 Re: [Metamath] mmj2 error js does not exist David A. Wheeler
2023/03/02 Re: [Metamath] Future website directions Thierry Arnoux
2023/03/02 Re: [Metamath] Future website directions David A. Wheeler
2023/03/02 [Metamath] mmj2 error js does not exist William Mitchell Jr
2023/03/01 [Metamath] Metamath website - current status David A. Wheeler
2023/02/27 Re: [Metamath] Future website directions Thierry Arnoux