metamath  

Messages by Date

• 2024/05/25 Re: [Metamath] Re: Blueprints for Metamath 'Thierry Arnoux' via Metamath
• 2024/05/25 Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. 'Thierry Arnoux' via Metamath
• 2024/05/24 [Metamath] Re: Blueprints for Metamath savask
• 2024/05/24 Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. Marshall Stoner
• 2024/05/24 Re: [Metamath] AKS Working Group 'Thierry Arnoux' via Metamath
• 2024/05/24 Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database. 'David A. Wheeler' via Metamath
• 2024/05/24 Re: [Metamath] Test if mailing list is working Dirk-Anton Broersen
• 2024/05/24 Re: Re: [Metamath] Test if mailing list is working 'Meta Kunt' via Metamath
• 2024/05/24 [Metamath] AKS Working Group 'asdf asdf' via Metamath
• 2024/05/24 [Metamath] Blueprints for Metamath 'Thierry Arnoux' via Metamath
• 2024/05/23 [Metamath] Putting typesetting "extra spaces" rules in .mm database. Marshall Stoner
• 2024/05/22 Re: [Metamath] Test if mailing list is working Jim Kingdon
• 2024/05/22 [Metamath] Test if mailing list is working 'asdf asdf' via Metamath
• 2024/05/16 Re: [Metamath] Feedback from metakunt, a recent contributor Jim Kingdon
• 2024/05/16 [Metamath] Re: Feedback from metakunt, a recent contributor samiro.d...@rwth-aachen.de
• 2024/05/16 [Metamath] Feedback from metakunt, a recent contributor 'ookami' via Metamath
• 2024/05/11 [Metamath] Re: I'm writing a more "explanatory" database. Marshall Stoner
• 2024/05/08 Re: [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
• 2024/05/06 Re: [Metamath] Mnemonic of Fr 'Alexander van der Vekens' via Metamath
• 2024/05/06 Re: [Metamath] Mnemonic of Fr 'Alexander van der Vekens' via Metamath
• 2024/05/02 Re: [Metamath] Question abouot indistopon Mario Carneiro
• 2024/05/01 Re: [Metamath] Mnemonic of Fr heiphohmia via Metamath
• 2024/05/01 Re: [Metamath] Question abouot indistopon 'B. Wilson' via Metamath
• 2024/05/01 Re: [Metamath] Mnemonic of Fr Mario Carneiro
• 2024/05/01 [Metamath] Mnemonic of Fr 'B. Wilson' via Metamath
• 2024/04/30 Re: [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
• 2024/04/28 Re: [Metamath] Re: The Ackermann function Jim Kingdon
• 2024/04/28 Re: [Metamath] Re: The Ackermann function 'Thierry Arnoux' via Metamath
• 2024/04/28 Re: [Metamath] Results about ax-13 usage 'Alexander van der Vekens' via Metamath
• 2024/04/28 [Metamath] Re: I'm writing a more "explanatory" database. 'Alexander van der Vekens' via Metamath
• 2024/04/28 [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
• 2024/04/28 [Metamath] Re: The Ackermann function 'Alexander van der Vekens' via Metamath
• 2024/04/28 [Metamath] The Ackermann function 'Alexander van der Vekens' via Metamath
• 2024/04/24 Re: [Metamath] Question abouot indistopon Mario Carneiro
• 2024/04/24 Re: [Metamath] Question abouot indistopon heiphohmia via Metamath
• 2024/04/23 Re: [Metamath] Question abouot indistopon Jim Kingdon
• 2024/04/22 [Metamath] Question abouot indistopon 'B. Wilson' via Metamath
• 2024/04/20 Re: [Metamath] Results about ax-13 usage Gino Giotto
• 2024/04/14 AW: [Metamath] Uncompressed proofs Discher, Samiro
• 2024/04/14 [Metamath] Uncompressed proofs 'Andrew Thompson Thompson' via Metamath
• 2024/04/07 Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
• 2024/04/06 Re: [Metamath] Trying to understand 2p2e4 Gino Giotto
• 2024/04/05 Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
• 2024/04/02 Re: [Metamath] Trying to understand 2p2e4 Mario Carneiro
• 2024/04/02 Re: [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
• 2024/04/02 Re: [Metamath] Trying to understand 2p2e4 Gino Giotto
• 2024/04/01 Re: [Metamath] Trying to understand 2p2e4 Mario Carneiro
• 2024/04/01 [Metamath] Trying to understand 2p2e4 Anarcocap-socdem
• 2024/03/30 Re: [Metamath] Re: Meaning of "JFM" Mario Carneiro
• 2024/03/30 [Metamath] Re: Meaning of "JFM" Glauco
• 2024/03/30 [Metamath] Meaning of "JFM" 'Alexander van der Vekens' via Metamath
• 2024/03/24 [Metamath] Success with Hmm, metamath-test, and metamath-docker Antony Bartlett
• 2024/03/19 Re: [Metamath] Help building hmm (Haskell Metamath verifier) Antony Bartlett
• 2024/03/18 Re: [Metamath] Help building hmm (Haskell Metamath verifier) Mario Carneiro
• 2024/03/18 Re: [Metamath] Help building hmm (Haskell Metamath verifier) Mario Carneiro
• 2024/03/18 [Metamath] Help building hmm (Haskell Metamath verifier) Antony Bartlett
• 2024/03/17 Re: [Metamath] metamath-test added to metamath-cmds docker image Mario Carneiro
• 2024/03/17 Re: [Metamath] metamath-test added to metamath-cmds docker image Antony Bartlett
• 2024/03/16 Re: [Metamath] metamath-test added to metamath-cmds docker image Mario Carneiro
• 2024/03/16 [Metamath] metamath-test added to metamath-cmds docker image Antony Bartlett
• 2024/03/12 Re: [Metamath] Results about ax-13 usage Mario Carneiro
• 2024/03/11 Re: [Metamath] Results about ax-13 usage Marshall Stoner
• 2024/03/11 Re: [Metamath] Results about ax-13 usage Jim Kingdon
• 2024/03/11 Re: [Metamath] Results about ax-13 usage Mario Carneiro
• 2024/03/10 [Metamath] Re: Yamma demo video Glauco
• 2024/03/10 [Metamath] Re: Yamma demo video Gino Giotto
• 2024/03/10 [Metamath] Re: Yamma demo video Glauco
• 2024/03/10 [Metamath] Yamma demo video Glauco
• 2024/03/10 Re: [Metamath] Results about ax-13 usage Gino Giotto
• 2024/03/09 Re: [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Glauco
• 2024/03/04 [Metamath] Release of pmGenerator 1.2: User-definable systems, and proof minimization challenges samiro.d...@rwth-aachen.de
• 2024/03/03 Re: [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer
• 2024/02/29 [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages bil...@gmail.com
• 2024/02/28 [Metamath] Re: [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Glauco
• 2024/02/28 [Metamath] [RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer
• 2024/02/24 [Metamath] Re: Yamma Glauco
• 2024/02/12 Re: [Metamath] Re: Proof generation Mario Carneiro
• 2024/02/12 [Metamath] Re: Proof generation jagra
• 2024/02/12 Re: [Metamath] Re: Proof generation Mario Carneiro
• 2024/02/12 [Metamath] Re: Proof generation Glauco
• 2024/02/11 Re: [Metamath] Proof generation Mario Carneiro
• 2024/02/11 [Metamath] Proof generation Jorge Agra
• 2024/02/07 [Metamath] Re: mm-web-rs server support Mario Carneiro
• 2024/02/07 [Metamath] Re: mm-web-rs server support Mario Carneiro
• 2024/02/07 [Metamath] Re: searching for theorem manually in Metamath lamp/ Marshall Stoner
• 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 bil...@gmail.com
• 2023/10/11 Re: [Metamath] Question on definition of magma Mario Carneiro
• 2023/10/11 Re: [Metamath] Question on definition of magma bil...@gmail.com
• 2023/10/11 Re: [Metamath] Question on definition of magma Mario Carneiro
• 2023/10/11 [Metamath] Question on definition of magma bil...@gmail.com
• 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

• Earlier messages