metamath  

Messages by Thread

• • Re: [Metamath] Same alphabet requirements in Word theorems David A. Wheeler
  • Re: [Metamath] Same alphabet requirements in Word theorems Jerry James
  • Re: [Metamath] Same alphabet requirements in Word theorems 'Alexander van der Vekens' via Metamath
• [Metamath] Metamath Christmas challenge savask
  • [Metamath] Re: Metamath Christmas challenge Glauco
  • [Metamath] Re: Metamath Christmas challenge Igor Ieskov
  • [Metamath] Re: Metamath Christmas challenge savask
  • [Metamath] Re: Metamath Christmas challenge Glauco
  • Re: [Metamath] Metamath Christmas challenge 'Thierry Arnoux' via Metamath
  • Re: [Metamath] Metamath Christmas challenge savask
  • Re: [Metamath] Metamath Christmas challenge 'Thierry Arnoux' via Metamath
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge savask
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge savask
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge David A. Wheeler
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge savask
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge savask
  • Re: [Metamath] Metamath Christmas challenge Igor Ieskov
  • Re: [Metamath] Metamath Christmas challenge savask
• [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] German translation of the Metamath book Mario Carneiro
  • Re: [Metamath] German translation of the Metamath book Jim Kingdon
  • Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
  • AW: [Metamath] German translation of the Metamath book Discher, Samiro
  • Re: [Metamath] German translation of the Metamath book Dirk-Anton Broersen
  • AW: [Metamath] German translation of the Metamath book Discher, Samiro
  • Re: [Metamath] German translation of the Metamath book 'Thierry Arnoux' via Metamath
  • Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] German translation of the Metamath book 'Alexander van der Vekens' via Metamath
• [Metamath] mm0 semantic equivalence Olof
  • Re: [Metamath] mm0 semantic equivalence Mario Carneiro
  • Re: [Metamath] mm0 semantic equivalence Olof
• [Metamath] renames of syl theorems Jim Kingdon
  • [Metamath] Re: renames of syl theorems Glauco
• [Metamath] Website is down Rohan Ridenour
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Thierry Arnoux
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Thierry Arnoux
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Jim Kingdon
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down BTernary Tau
  • AW: [Metamath] Website is down Discher, Samiro
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Gino Giotto
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Mario Carneiro
  • Re: [Metamath] Website is down Mario Carneiro
• [Metamath] Order of variables in DV statements 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Order of variables in DV statements Mario Carneiro
  • Re: [Metamath] Order of variables in DV statements BTernary Tau
  • Re: [Metamath] Order of variables in DV statements Igor Ieskov
• [Metamath] Question on definition of magma [email protected]
  • Re: [Metamath] Question on definition of magma Mario Carneiro
  • Re: [Metamath] Question on definition of magma [email protected]
  • Re: [Metamath] Question on definition of magma Mario Carneiro
  • Re: [Metamath] Question on definition of magma [email protected]
  • Re: [Metamath] Question on definition of magma Mario Carneiro
• [Metamath] naming of syl theorems Jim Kingdon
• [Metamath] What's the procedure for moving a theorem out of someone else's mathbox? BTernary Tau
  • Re: [Metamath] What's the procedure for moving a theorem out of someone else's mathbox? Steven Nguyen
• [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Jim Kingdon
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Benoit
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Jim Kingdon
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Benoit
  • Re: [Metamath] Update: website generation rewrite Mario Carneiro
  • Re: [Metamath] Update: website generation rewrite Benoit
• [Metamath] Question on Theorem pm2.61ne [email protected]
  • Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
  • [Metamath] Question on Theorem pm2.61ne [email protected]
  • Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
  • Re: [Metamath] Question on Theorem pm2.61ne [email protected]
  • Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
• [Metamath] fnconstg [email protected]
  • Re: [Metamath] fnconstg Thierry Arnoux
  • Re: [Metamath] fnconstg Jim Kingdon
  • Re: [Metamath] fnconstg 'Alexander van der Vekens' via Metamath
• [Metamath] Metamath Website not loading Sophie
  • Re: [Metamath] Metamath Website not loading Jim Kingdon
  • AW: [Metamath] Metamath Website not loading Discher, Samiro
  • AW: [Metamath] Metamath Website not loading Discher, Samiro
  • Re: [Metamath] Metamath Website not loading CreateSource
  • Re: [Metamath] Metamath Website not loading [email protected]
  • Re: [Metamath] Metamath Website not loading David A. Wheeler
  • Re: [Metamath] Metamath Website not loading Jim Kingdon
  • Re: [Metamath] Metamath Website not loading heiphohmia via Metamath
  • Re: [Metamath] Metamath Website not loading Jim Kingdon
  • Re: [Metamath] Metamath Website not loading heiphohmia via Metamath
• [Metamath] Metamath-lamp version 17 released Igor Ieskov
• [Metamath] Did someone train a LLM on the set.mm 'Marcel Richter' via Metamath
  • Re: [Metamath] Did someone train a LLM on the set.mm Amaury Hayat
  • Re: [Metamath] Did someone train a LLM on the set.mm David A. Wheeler
• [Metamath] Announcing an additional Metamath 100 Theorem for iset.mm Jim Kingdon
• [Metamath] Trouble understanding Deduction style Jeroen van Rensen
  • Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
  • Re: [Metamath] Trouble understanding Deduction style David A. Wheeler
  • Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
  • Re: [Metamath] Trouble understanding Deduction style David A. Wheeler
  • Re: [Metamath] Trouble understanding Deduction style Jim Kingdon
  • Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
  • Re: [Metamath] Trouble understanding Deduction style Marshall Stoner
  • Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
  • Re: [Metamath] Trouble understanding Deduction style Thierry Arnoux
  • Re: [Metamath] Trouble understanding Deduction style Jeroen van Rensen
  • Re: [Metamath] Trouble understanding Deduction style Thierry Arnoux
• [Metamath] ?Statement "a3" cannot be unified with step 25. Jeroen van Rensen
  • Re: [Metamath] ?Statement "a3" cannot be unified with step 25. Mario Carneiro
  • Re: [Metamath] ?Statement "a3" cannot be unified with step 25. Jeroen van Rensen
• [Metamath] Substitute wff for a variable Jeroen van Rensen
  • Re: [Metamath] Substitute wff for a variable Mario Carneiro
  • Re: [Metamath] Substitute wff for a variable Mario Carneiro
  • Re: [Metamath] Substitute wff for a variable Jeroen van Rensen
• [Metamath] Proposed rename of mpt2 abbreviation to mpo Jim Kingdon
• [Metamath] Metamath-lamp version 16 released Igor Ieskov
• [Metamath] Can anyone tell me where to find an explanation of the .mmp format? Marshall Stoner
  • [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Glauco
  • [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Marshall Stoner
  • [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Glauco
  • [Metamath] Re: Can anyone tell me where to find an explanation of the .mmp format? Igor Ieskov
• [Metamath] Is it legitimate to assert a propositional function? 'Bulhwi Cha' via Metamath
  • [Metamath] Re: Is it legitimate to assert a propositional function? 'Bulhwi Cha' via Metamath
  • Re: [Metamath] Is it legitimate to assert a propositional function? Ken Kubota
• [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
  • Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
  • Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
  • Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space David A. Wheeler
• [Metamath] A bug in the MINIMIZE_WITH command ? Benoit
  • [Metamath] Re: A bug in the MINIMIZE_WITH command ? Gino Giotto
  • [Metamath] Re: A bug in the MINIMIZE_WITH command ? Benoit
• [Metamath] Metamath-lamp version 15 released (minor UI improvements) Igor Ieskov
• [Metamath] Submitting a theorem to set.mm Larry Lesyna
  • Re: [Metamath] Submitting a theorem to set.mm Jim Kingdon
  • Re: [Metamath] Submitting a theorem to set.mm David A. Wheeler
  • Re: [Metamath] Submitting a theorem to set.mm Mázsa Péter
  • Re: [Metamath] Submitting a theorem to set.mm llesyna
• [Metamath] Reminder: We still have Metamath 100 entries to complete!! David A. Wheeler
  • Re: [Metamath] Reminder: We still have Metamath 100 entries to complete!! Jim Kingdon
• [Metamath] Metamath-lamp version 14 released, now with undo David A. Wheeler
  • Re: [Metamath] Metamath-lamp version 14 released, now with undo David A. Wheeler
  • Re: [Metamath] Metamath-lamp version 14 released, now with undo Marshall Stoner
• [Metamath] The Math Genome Project - feedback request Johnathan Mercer
  • AW: [Metamath] The Math Genome Project - feedback request Discher, Samiro
  • Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer
  • Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer
  • Re: [Metamath] The Math Genome Project - feedback request Steven Nguyen
  • Re: [Metamath] The Math Genome Project - feedback request Johnathan Mercer
• [Metamath] How do you quickly jump to the markup definitions in set.mm? Marshall Stoner
  • [Metamath] Re: How do you quickly jump to the markup definitions in set.mm? Marshall Stoner
• [Metamath] Metamath-lamp version 13 released David Wheeler
• Re: [Metamath] I cannot open mmj2: mmj.pa.MMJException: E-UT-1502 Error Mázsa Péter
• [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. David A. Wheeler
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. David A. Wheeler
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Ken Kubota
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Johnathan Mercer
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Ken Kubota
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Mario Carneiro
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Marshall Stoner
  • Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm. Jim Kingdon
• [Metamath] Metamath is famous! Tau Day famous that is Jim Kingdon
• [Metamath] Metamath-lamp version 11 has been released! David A. Wheeler
• [Metamath] Updated video of "Introduction to Metamath-lamp, part 2" David A . Wheeler
  • [Metamath] Video of "Introduction to Metamath-lamp, part 3" David Wheeler
  • [Metamath] Re: Video of "Introduction to Metamath-lamp, part 3" Igor Ieskov
  • Re: [Metamath] Video of "Introduction to Metamath-lamp, part 3" David A. Wheeler
• [Metamath] Metamath-lamp video, part 1 David A. Wheeler
  • [Metamath] Draft Metamath-lamp video, part **2** David A. Wheeler
  • Re: [Metamath] Metamath-lamp video, part 1 Jim Kingdon

• Earlier messages
• Later messages