metamath  

Messages by Thread

• [Metamath] Metamath website page updates continue David A. Wheeler
• [Metamath] Is there a way to show all mandatory hypotheses of a statement on the Metamath program? Humanities Clinic
• [Metamath] Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
  • [Metamath] Re: Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
  • [Metamath] Re: Is there a way to display/list statements and symbols of a certain type in Metamath? Humanities Clinic
• [Metamath] kids these days Jim Kingdon
• [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
  • Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it Jim Kingdon
  • Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it Paul Chapman
  • Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
  • Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it David A. Wheeler
• [Metamath] How are typecodes used/enforced by the Metamath program? Humanities Clinic
  • [Metamath] Re: How are typecodes used/enforced by the Metamath program? Humanities Clinic
  • Re: [Metamath] How are typecodes used/enforced by the Metamath program? Mario Carneiro
  • Re: [Metamath] How are typecodes used/enforced by the Metamath program? David A. Wheeler
• [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
  • AW: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Discher, Samiro
  • Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
  • Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? David A. Wheeler
  • Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Humanities Clinic
  • Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Jim Kingdon
  • Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional? Thierry Arnoux
• [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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
• [Metamath] How to Understand The "More Complicated" Expressions in Definitions Humanities Clinic
  • Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Mario Carneiro
  • Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Jim Kingdon
  • Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions Thierry Arnoux
• [Metamath] "Metamath-lamp Guide" now visible at: https://lamp-guide.metamath.org/ David A. Wheeler
• [Metamath] I intend to create a new metamath org repository named "lamp-guide" David A. Wheeler
  • [Metamath] Re: I intend to create a new metamath org repository named "lamp-guide" David A. Wheeler
• [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Humanities Clinic
  • Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Mario Carneiro
  • Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html? Jim Kingdon
• [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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
• [Metamath] eqsb3lem vs eqsb3v Zheng Fan
  • Re: [Metamath] eqsb3lem vs eqsb3v David A. Wheeler
  • Re: [Metamath] eqsb3lem vs eqsb3v Zheng Fan
  • Re: [Metamath] eqsb3lem vs eqsb3v 'Alexander van der Vekens' via Metamath
• [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d LM
  • Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d Mario Carneiro
  • Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d Mario Carneiro
  • Re: [Metamath] eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d LM
• [Metamath] mmj2 Export GMMF LM
  • Re: [Metamath] mmj2 Export GMMF Mázsa Péter
  • Re: [Metamath] mmj2 Export GMMF LM
  • Re: [Metamath] mmj2 Export GMMF LM
• [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) LM
  • Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Mario Carneiro
  • Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Igor Ieskov
  • Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) LM
  • Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style) Jim Kingdon
• [Metamath] Reverse polish notation proofs from first principles exclusively Guram Mikaberidze
  • Re: [Metamath] Reverse polish notation proofs from first principles exclusively Mario Carneiro
  • [Metamath] Re: Reverse polish notation proofs from first principles exclusively Samiro Discher
  • [Metamath] Re: Reverse polish notation proofs from first principles exclusively Samiro Discher
• [Metamath] mmj2 compact representation for $d statements Glauco
  • [Metamath] Re: mmj2 compact representation for $d statements Benoit
  • Re: [Metamath] Re: mmj2 compact representation for $d statements Mario Carneiro
  • Re: [Metamath] Re: mmj2 compact representation for $d statements Mario Carneiro
  • Re: [Metamath] Re: mmj2 compact representation for $d statements Glauco
  • Re: [Metamath] Re: mmj2 compact representation for $d statements Glauco
• [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
  • [Metamath] Re: Speculations on how to help machine learning systems generate metamath proofs Jon P
  • Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
  • Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs Jon P
  • Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs David A. Wheeler
  • Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs Jon P
• [Metamath] Negative use cases database? Samuel Goto
  • Re: [Metamath] Negative use cases database? Mario Carneiro
  • Re: [Metamath] Negative use cases database? Jim Kingdon
  • [Metamath] Re: Negative use cases database? Glauco
• [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist David A. Wheeler
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist David A. Wheeler
  • Re: [Metamath] mmj2 error js does not exist David Crisp
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist David Crisp
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist Mario Carneiro
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist jannik vierling
  • Re: [Metamath] mmj2 error js does not exist William Mitchell Jr
  • Re: [Metamath] mmj2 error js does not exist Benoit
  • Re: [Metamath] mmj2 error js does not exist David A. Wheeler
  • Re: [Metamath] mmj2 error js does not exist jannik vierling
  • Re: [Metamath] mmj2 error js does not exist David A. Wheeler
• [Metamath] Metamath website - current status David A. Wheeler
  • [Metamath] Re: Metamath website - current status Glauco
  • [Metamath] Re: Metamath website - current status Samiro Discher
• [Metamath] Metamatix Thierry Arnoux
  • Re: [Metamath] Metamatix David A. Wheeler
  • Re: [Metamath] Metamatix Thierry Arnoux
  • Re: [Metamath] Metamatix Denis Carnier
  • Re: [Metamath] Metamatix Mario Carneiro
• [Metamath] Re: An exhaustive generator for the mmsolitaire project Samiro Discher
  • [Metamath] Re: An exhaustive generator for the mmsolitaire project Samiro Discher
• [Metamath] Formalizing Fermat's Last Theorem Jim Kingdon
  • [Metamath] Re: Formalizing Fermat's Last Theorem Steven Nguyen
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Jim Kingdon
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem David Crisp
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Jim Kingdon
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Mario Carneiro
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem LM
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Glauco
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Paul Chapman
  • Re: [Metamath] Re: Formalizing Fermat's Last Theorem Antony Bartlett
• Re: [Metamath] shorter proofs for some theorems in set.mm David A. Wheeler
  • Re: [Metamath] shorter proofs for some theorems in set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] shorter proofs for some theorems in set.mm Igor Ieskov
  • Re: [Metamath] shorter proofs for some theorems in set.mm David A. Wheeler
  • Re: [Metamath] shorter proofs for some theorems in set.mm Benoit
  • Re: [Metamath] shorter proofs for some theorems in set.mm Benoit
  • Re: [Metamath] shorter proofs for some theorems in set.mm Igor Ieskov
  • Re: [Metamath] shorter proofs for some theorems in set.mm Thierry Arnoux
• [Metamath] Fyi: Linode rebrand David A. Wheeler
  • Re: [Metamath] Fyi: Linode rebrand heiphohmia via Metamath
• [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • [Metamath] Re: Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Jon P
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Johnathan Mercer
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Jon P
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Auguste Poiroux
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Cris Perdue
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Antony Bartlett
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Mario Carneiro
  • Re: [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Jon P
  • Re: [Metamath] Future website directions Mario Carneiro
  • Re: [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Mario Carneiro
  • Re: [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Thierry Arnoux
  • Re: [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Thierry Arnoux
  • Re: [Metamath] Future website directions Mario Carneiro
  • Re: [Metamath] Future website directions David A. Wheeler
  • Re: [Metamath] Future website directions Mario Carneiro
  • Re: [Metamath] Future website directions Antony Bartlett
  • Re: [Metamath] Future website directions Glauco
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Cris Perdue
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Igor Ieskov
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David Wheeler
  • Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Igor Ieskov
  • [Metamath] Re: Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Benoit
• [Metamath] Hardened us.metamath.org David A. Wheeler

• Earlier messages
• Later messages