metamath  

Messages by Thread

• [Metamath] AKS Working Group 'asdf asdf' via Metamath
  • Re: [Metamath] AKS Working Group 'Thierry Arnoux' via Metamath
• [Metamath] Blueprints for Metamath 'Thierry Arnoux' via Metamath
  • [Metamath] Re: Blueprints for Metamath savask
  • Re: [Metamath] Re: Blueprints for Metamath 'Thierry Arnoux' via Metamath
• [Metamath] Putting typesetting "extra spaces" rules in .mm database. Marshall Stoner
  • Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. 'David A. Wheeler' via Metamath
  • Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. Marshall Stoner
  • Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. 'Thierry Arnoux' via Metamath
• [Metamath] Test if mailing list is working 'asdf asdf' via Metamath
  • Re: [Metamath] Test if mailing list is working Jim Kingdon
  • Re: Re: [Metamath] Test if mailing list is working 'Meta Kunt' via Metamath
  • Re: [Metamath] Test if mailing list is working Dirk-Anton Broersen
• [Metamath] Feedback from metakunt, a recent contributor 'ookami' via Metamath
  • [Metamath] Re: Feedback from metakunt, a recent contributor samiro.d...@rwth-aachen.de
  • Re: [Metamath] Feedback from metakunt, a recent contributor Jim Kingdon
• [Metamath] Mnemonic of Fr 'B. Wilson' via Metamath
  • Re: [Metamath] Mnemonic of Fr Mario Carneiro
  • Re: [Metamath] Mnemonic of Fr heiphohmia via Metamath
  • Re: [Metamath] Mnemonic of Fr 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Mnemonic of Fr 'Alexander van der Vekens' via Metamath
• [Metamath] Re: I'm writing a more "explanatory" database. 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: I'm writing a more "explanatory" database. Marshall Stoner
• [Metamath] The Ackermann function 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: The Ackermann function 'Thierry Arnoux' via Metamath
  • Re: [Metamath] Re: The Ackermann function Jim Kingdon
  • Re: [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
• [Metamath] Question abouot indistopon 'B. Wilson' via Metamath
  • Re: [Metamath] Question abouot indistopon Jim Kingdon
  • Re: [Metamath] Question abouot indistopon heiphohmia via Metamath
  • Re: [Metamath] Question abouot indistopon Mario Carneiro
  • Re: [Metamath] Question abouot indistopon 'B. Wilson' via Metamath
  • Re: [Metamath] Question abouot indistopon Mario Carneiro
• [Metamath] Uncompressed proofs 'Andrew Thompson Thompson' via Metamath
  • AW: [Metamath] Uncompressed proofs Discher, Samiro
• [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
  • Re: [Metamath] Trying to understand 2p2e4 Mario Carneiro
  • Re: [Metamath] Trying to understand 2p2e4 Gino Giotto
  • Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
  • Re: [Metamath] Trying to understand 2p2e4 Mario Carneiro
  • Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
  • Re: [Metamath] Trying to understand 2p2e4 Gino Giotto
  • Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
• [Metamath] Meaning of "JFM" 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Meaning of "JFM" Glauco
  • Re: [Metamath] Re: Meaning of "JFM" Mario Carneiro
• [Metamath] Success with Hmm, metamath-test, and metamath-docker Antony Bartlett
• [Metamath] Help building hmm (Haskell Metamath verifier) Antony Bartlett
  • Re: [Metamath] Help building hmm (Haskell Metamath verifier) Mario Carneiro
  • Re: [Metamath] Help building hmm (Haskell Metamath verifier) Mario Carneiro
  • Re: [Metamath] Help building hmm (Haskell Metamath verifier) Antony Bartlett
• [Metamath] metamath-test added to metamath-cmds docker image Antony Bartlett
  • Re: [Metamath] metamath-test added to metamath-cmds docker image Mario Carneiro
  • Re: [Metamath] metamath-test added to metamath-cmds docker image Antony Bartlett
  • Re: [Metamath] metamath-test added to metamath-cmds docker image Mario Carneiro
• [Metamath] Yamma demo video Glauco
  • [Metamath] Re: Yamma demo video Glauco
  • [Metamath] Re: Yamma demo video Gino Giotto
  • [Metamath] Re: Yamma demo video Glauco
• [Metamath] Release of pmGenerator 1.2: User-definable systems, and proof minimization challenges samiro.d...@rwth-aachen.de
• [Metamath] [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer
  • [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Glauco
  • [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages bil...@gmail.com
  • Re: [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer
  • Re: [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Glauco
• [Metamath] Proof generation Jorge Agra
  • Re: [Metamath] Proof generation Mario Carneiro
  • [Metamath] Re: Proof generation Glauco
  • Re: [Metamath] Re: Proof generation Mario Carneiro
  • [Metamath] Re: Proof generation jagra
  • Re: [Metamath] Re: Proof generation Mario Carneiro
• [Metamath] searching for theorem manually in Metamath lamp/ Marshall Stoner
  • [Metamath] Re: searching for theorem manually in Metamath lamp/ Igor Ieskov
  • [Metamath] Re: searching for theorem manually in Metamath lamp/ Marshall Stoner
• [Metamath] Constant symbols are not allowed in a "$d" statement. Brian Larson
  • Re: [Metamath] Constant symbols are not allowed in a "$d" statement. Mario Carneiro
• [Metamath] mmj2: Unification failure in derivation proof step Brian Larson
  • Re: [Metamath] mmj2: Unification failure in derivation proof step Mario Carneiro
  • Re: [Metamath] mmj2: Unification failure in derivation proof step Brian Larson
  • Re: [Metamath] mmj2: Unification failure in derivation proof step Mario Carneiro
• [Metamath] Prime Number Theorem Jim Kingdon
  • Re: [Metamath] Prime Number Theorem 'Thierry Arnoux' via Metamath
  • Re: [Metamath] Prime Number Theorem Mario Carneiro
  • Re: [Metamath] Prime Number Theorem Jim Kingdon
  • Re: [Metamath] Prime Number Theorem savask
• [Metamath] Prime Ideals 'Thierry Arnoux' via Metamath
• Re: [Metamath] Re: Area of a triangle (was: Help with beginning to contribute to set.mm) Benoit
• [Metamath] Results about ax-13 usage Gino Giotto
  • Re: [Metamath] Results about ax-13 usage Jim Kingdon
  • Re: [Metamath] Results about ax-13 usage Mario Carneiro
  • Re: [Metamath] Results about ax-13 usage Benoit
  • Re: [Metamath] Results about ax-13 usage Gino Giotto
  • Re: [Metamath] Results about ax-13 usage Mario Carneiro
  • Re: [Metamath] Results about ax-13 usage Mario Carneiro
  • Re: [Metamath] Results about ax-13 usage Jim Kingdon
  • Re: [Metamath] Results about ax-13 usage Gino Giotto
  • Re: [Metamath] Results about ax-13 usage Mario Carneiro
  • Re: [Metamath] Results about ax-13 usage Jim Kingdon
  • Re: [Metamath] Results about ax-13 usage Mario Carneiro
  • Re: [Metamath] Results about ax-13 usage Gino Giotto
  • Re: [Metamath] Results about ax-13 usage 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Results about ax-13 usage Marshall Stoner
• [Metamath] Same alphabet requirements in Word theorems Jerry James
  • 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 bil...@gmail.com
  • Re: [Metamath] Question on definition of magma Mario Carneiro
  • Re: [Metamath] Question on definition of magma bil...@gmail.com
  • Re: [Metamath] Question on definition of magma Mario Carneiro
  • Re: [Metamath] Question on definition of magma bil...@gmail.com
  • 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 bil...@gmail.com
  • Re: [Metamath] Question on Theorem pm2.61ne Mario Carneiro
  • [Metamath] Question on Theorem pm2.61ne bil...@gmail.com

• Earlier messages