metamath  

Messages by Date

• 2024/02/05 [Metamath] Re: searching for theorem manually in Metamath lamp/ Igor Ieskov
• 2024/02/05 [Metamath] searching for theorem manually in Metamath lamp/ Marshall Stoner
• 2024/02/03 Re: [Metamath] Constant symbols are not allowed in a "$d" statement. Mario Carneiro
• 2024/02/03 [Metamath] Constant symbols are not allowed in a "$d" statement. Brian Larson
• 2024/02/02 Re: [Metamath] Prime Number Theorem savask
• 2024/02/02 Re: [Metamath] mmj2: Unification failure in derivation proof step Mario Carneiro
• 2024/02/02 Re: [Metamath] mmj2: Unification failure in derivation proof step Brian Larson
• 2024/02/02 Re: [Metamath] mmj2: Unification failure in derivation proof step Mario Carneiro
• 2024/02/01 Re: [Metamath] Prime Number Theorem Jim Kingdon
• 2024/02/01 [Metamath] mmj2: Unification failure in derivation proof step Brian Larson
• 2024/01/31 Re: [Metamath] Prime Number Theorem Mario Carneiro
• 2024/01/31 Re: [Metamath] Prime Number Theorem 'Thierry Arnoux' via Metamath
• 2024/01/30 [Metamath] Prime Number Theorem Jim Kingdon
• 2024/01/17 Re: [Metamath] Metamath Christmas challenge savask
• 2024/01/17 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/17 [Metamath] Prime Ideals 'Thierry Arnoux' via Metamath
• 2024/01/16 Re: [Metamath] Metamath Christmas challenge savask
• 2024/01/15 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/15 Re: [Metamath] Metamath Christmas challenge savask
• 2024/01/15 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/14 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/10 Re: [Metamath] Results about ax-13 usage Jim Kingdon
• 2024/01/09 Re: [Metamath] Results about ax-13 usage Mario Carneiro
• 2024/01/09 Re: [Metamath] Results about ax-13 usage Mario Carneiro
• 2024/01/09 Re: [Metamath] Results about ax-13 usage Gino Giotto
• 2024/01/09 Re: [Metamath] Same alphabet requirements in Word theorems 'Alexander van der Vekens' via Metamath
• 2024/01/06 Re: [Metamath] Re: Area of a triangle (was: Help with beginning to contribute to set.mm) Benoit
• 2024/01/03 Re: [Metamath] Same alphabet requirements in Word theorems Jerry James
• 2024/01/03 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/02 Re: [Metamath] Results about ax-13 usage Benoit
• 2024/01/02 Re: [Metamath] Metamath Christmas challenge David A. Wheeler
• 2024/01/02 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/02 Re: [Metamath] Metamath Christmas challenge savask
• 2024/01/01 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2024/01/01 Re: [Metamath] Results about ax-13 usage Mario Carneiro
• 2024/01/01 Re: [Metamath] Results about ax-13 usage Jim Kingdon
• 2024/01/01 Re: [Metamath] Same alphabet requirements in Word theorems David A. Wheeler
• 2024/01/01 [Metamath] Results about ax-13 usage Gino Giotto
• 2023/12/31 [Metamath] Same alphabet requirements in Word theorems Jerry James
• 2023/12/18 Re: [Metamath] Metamath Christmas challenge savask
• 2023/12/18 Re: [Metamath] Metamath Christmas challenge Igor Ieskov
• 2023/12/17 Re: [Metamath] Metamath Christmas challenge 'Thierry Arnoux' via Metamath
• 2023/12/17 Re: [Metamath] Metamath Christmas challenge savask
• 2023/12/17 Re: [Metamath] Metamath Christmas challenge 'Thierry Arnoux' via Metamath
• 2023/12/12 Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
• 2023/12/11 [Metamath] Re: Metamath Christmas challenge Glauco
• 2023/12/11 [Metamath] Re: Metamath Christmas challenge savask
• 2023/12/10 [Metamath] Re: Metamath Christmas challenge Igor Ieskov
• 2023/12/10 [Metamath] Re: Metamath Christmas challenge Glauco
• 2023/12/10 [Metamath] Metamath Christmas challenge savask
• 2023/12/08 Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
• 2023/12/07 Re: [Metamath] German translation of the Metamath book 'Thierry Arnoux' via Metamath
• 2023/12/05 AW: [Metamath] German translation of the Metamath book Discher, Samiro
• 2023/12/05 Re: [Metamath] German translation of the Metamath book Dirk-Anton Broersen
• 2023/12/05 AW: [Metamath] German translation of the Metamath book Discher, Samiro
• 2023/12/05 Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
• 2023/12/04 Re: [Metamath] German translation of the Metamath book Jim Kingdon
• 2023/12/03 Re: [Metamath] German translation of the Metamath book Mario Carneiro
• 2023/12/03 [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
• 2023/11/29 Re: [Metamath] mm0 semantic equivalence Olof
• 2023/11/28 Re: [Metamath] mm0 semantic equivalence Mario Carneiro
• 2023/11/28 [Metamath] mm0 semantic equivalence Olof
• 2023/11/26 Re: [Metamath] Re: Yamma Jim Kingdon
• 2023/11/26 Re: [Metamath] Re: Yamma Glauco
• 2023/11/26 Re: [Metamath] Re: Yamma Jim Kingdon
• 2023/11/26 [Metamath] Re: Yamma Glauco
• 2023/11/14 [Metamath] Re: Yamma Glauco
• 2023/11/14 [Metamath] Re: renames of syl theorems Glauco
• 2023/11/13 [Metamath] renames of syl theorems Jim Kingdon
• 2023/11/12 Re: [Metamath] Website is down Mario Carneiro
• 2023/11/12 Re: [Metamath] Website is down Mario Carneiro
• 2023/11/11 Re: [Metamath] Website is down Gino Giotto
• 2023/11/10 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/11/06 Re: [Metamath] Order of variables in DV statements Igor Ieskov
• 2023/10/28 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/28 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 AW: [Metamath] Website is down Discher, Samiro
• 2023/10/25 Re: [Metamath] Website is down BTernary Tau
• 2023/10/25 Re: [Metamath] Website is down Gino Giotto
• 2023/10/25 Re: [Metamath] Website is down Jim Kingdon
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Thierry Arnoux
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 Re: [Metamath] Website is down Thierry Arnoux
• 2023/10/25 Re: [Metamath] Website is down Mario Carneiro
• 2023/10/25 [Metamath] Website is down Rohan Ridenour
• 2023/10/18 Re: [Metamath] Order of variables in DV statements BTernary Tau
• 2023/10/17 Re: [Metamath] Order of variables in DV statements Mario Carneiro
• 2023/10/17 [Metamath] Order of variables in DV statements 'Alexander van der Vekens' via Metamath
• 2023/10/11 Re: [Metamath] Question on definition of magma Mario Carneiro
• 2023/10/11 Re: [Metamath] Question on definition of magma [email protected]
• 2023/10/11 Re: [Metamath] Question on definition of magma Mario Carneiro
• 2023/10/11 Re: [Metamath] Question on definition of magma [email protected]
• 2023/10/11 Re: [Metamath] Question on definition of magma Mario Carneiro
• 2023/10/11 [Metamath] Question on definition of magma [email protected]
• 2023/10/07 [Metamath] naming of syl theorems Jim Kingdon
• 2023/10/05 Re: [Metamath] What's the procedure for moving a theorem out of someone else's mathbox? Steven Nguyen
• 2023/10/04 [Metamath] What's the procedure for moving a theorem out of someone else's mathbox? BTernary Tau
• 2023/10/02 Re: [Metamath] Update: website generation rewrite Benoit
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Jim Kingdon
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Benoit
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Benoit
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/30 Re: [Metamath] Update: website generation rewrite Jim Kingdon
• 2023/09/29 [Metamath] Update: website generation rewrite Mario Carneiro
• 2023/09/29 Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
• 2023/09/29 Re: [Metamath] Question on Theorem pm2.61ne [email protected]
• 2023/09/29 Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
• 2023/09/29 [Metamath] Question on Theorem pm2.61ne [email protected]
• 2023/09/29 Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
• 2023/09/29 [Metamath] Question on Theorem pm2.61ne [email protected]
• 2023/09/26 Re: [Metamath] fnconstg 'Alexander van der Vekens' via Metamath
• 2023/09/23 Re: [Metamath] fnconstg Jim Kingdon
• 2023/09/22 Re: [Metamath] fnconstg Thierry Arnoux
• 2023/09/22 [Metamath] fnconstg [email protected]
• 2023/09/09 Re: [Metamath] Metamath Website not loading heiphohmia via Metamath
• 2023/09/09 Re: [Metamath] Metamath Website not loading Jim Kingdon
• 2023/09/09 Re: [Metamath] Metamath Website not loading heiphohmia via Metamath
• 2023/09/09 Re: [Metamath] Metamath Website not loading Jim Kingdon
• 2023/09/09 Re: [Metamath] Metamath Website not loading David A. Wheeler
• 2023/09/09 Re: [Metamath] Metamath Website not loading [email protected]
• 2023/09/08 Re: [Metamath] Metamath Website not loading CreateSource
• 2023/09/05 AW: [Metamath] Metamath Website not loading Discher, Samiro
• 2023/09/05 AW: [Metamath] Metamath Website not loading Discher, Samiro
• 2023/09/05 Re: [Metamath] Metamath Website not loading Jim Kingdon
• 2023/09/05 [Metamath] Metamath Website not loading Sophie
• 2023/08/28 [Metamath] Metamath-lamp version 17 released Igor Ieskov
• 2023/08/20 Re: [Metamath] Did someone train a LLM on the set.mm David A. Wheeler
• 2023/08/19 Re: [Metamath] Did someone train a LLM on the set.mm Amaury Hayat
• 2023/08/19 [Metamath] Did someone train a LLM on the set.mm 'Marcel Richter' via Metamath
• 2023/08/18 [Metamath] Announcing an additional Metamath 100 Theorem for iset.mm Jim Kingdon
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Thierry Arnoux
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Thierry Arnoux
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Marshall Stoner
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style David A. Wheeler
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style David A. Wheeler
• 2023/08/15 Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
• 2023/08/15 [Metamath] Trouble understanding Deduction style Jeroen van Rensen
• 2023/08/14 Re: [Metamath] ?Statement "a3" cannot be unified with step 25. Jeroen van Rensen
• 2023/08/13 Re: [Metamath] ?Statement "a3" cannot be unified with step 25. Mario Carneiro
• 2023/08/13 [Metamath] ?Statement "a3" cannot be unified with step 25. Jeroen van Rensen
• 2023/08/11 Re: [Metamath] Substitute wff for a variable Jeroen van Rensen
• 2023/08/11 Re: [Metamath] Substitute wff for a variable Mario Carneiro
• 2023/08/11 Re: [Metamath] Substitute wff for a variable Mario Carneiro
• 2023/08/11 [Metamath] Substitute wff for a variable Jeroen van Rensen
• 2023/08/09 [Metamath] Proposed rename of mpt2 abbreviation to mpo Jim Kingdon
• 2023/08/08 [Metamath] Metamath-lamp version 16 released Igor Ieskov
• 2023/08/07 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer sgoto
• 2023/08/03 [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Igor Ieskov
• 2023/07/31 [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Glauco
• 2023/07/30 [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Marshall Stoner
• 2023/07/30 [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Glauco
• 2023/07/30 Re: [Metamath] Is it legitimate to assert a propositional function? Ken Kubota
• 2023/07/30 [Metamath] Can anyone tell me where to find an explanation of the .mmp format? Marshall Stoner
• 2023/07/30 [Metamath] Re: Is it legitimate to assert a propositional function? 'Bulhwi Cha' via Metamath
• 2023/07/30 [Metamath] Is it legitimate to assert a propositional function? 'Bulhwi Cha' via Metamath
• 2023/07/28 [Metamath] Re: A bug in the MINIMIZE_WITH command ? Benoit
• 2023/07/26 Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
• 2023/07/26 [Metamath] Re: A bug in the MINIMIZE_WITH command ? Gino Giotto
• 2023/07/25 Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
• 2023/07/25 Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
• 2023/07/24 [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
• 2023/07/22 [Metamath] A bug in the MINIMIZE_WITH command ? Benoit
• 2023/07/22 [Metamath] Metamath-lamp version 15 released (minor UI improvements) Igor Ieskov
• 2023/07/18 Re: [Metamath] Submitting a theorem to set.mm llesyna
• 2023/07/18 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Ken Kubota
• 2023/07/18 Re: [Metamath] Submitting a theorem to set.mm Mázsa Péter
• 2023/07/17 Re: [Metamath] Submitting a theorem to set.mm David A. Wheeler
• 2023/07/17 Re: [Metamath] Submitting a theorem to set.mm Jim Kingdon
• 2023/07/17 [Metamath] Submitting a theorem to set.mm Larry Lesyna
• 2023/07/17 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Johnathan Mercer
• 2023/07/17 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Ken Kubota
• 2023/07/16 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. David A. Wheeler
• 2023/07/16 Re: [Metamath] Metamath-lamp version 14 released, now with undo Marshall Stoner
• 2023/07/16 Re: [Metamath] Reminder: We still have Metamath 100 entries to complete!! Jim Kingdon
• 2023/07/16 Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
• 2023/07/16 Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer
• 2023/07/16 Re: [Metamath] The Math Genome Project - feedback request Steven Nguyen
• 2023/07/14 Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer
• 2023/07/14 Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer

• Earlier messages
• Later messages