metamath  

Messages by Thread

• [Metamath] Small breaking change in mm-lamp Igor Ieskov
• [Metamath] Developing Galois theory in set.mm 'Meta Kunt' via Metamath
  • Re: [Metamath] Developing Galois theory in set.mm 'Thierry Arnoux' via Metamath
  • Re: [Metamath] Developing Galois theory in set.mm heiphohmia via Metamath
  • Re: [Metamath] Developing Galois theory in set.mm Steven Nguyen
  • Re: [Metamath] Developing Galois theory in set.mm heiphohmia via Metamath
  • [Metamath] Developing Galois theory in set.mm 'Meta Kunt' via Metamath
  • Re: [Metamath] Developing Galois theory in set.mm Jim Kingdon
• [Metamath] Question about a specific problem probably unrelated with metamath jagra
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath jagra
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Jorge Agra
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Mario Carneiro
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Glauco
  • Re: [Metamath] Question about a specific problem probably unrelated with metamath Igor Ieskov
• [Metamath] Google DeepMind's AlphaProof [email protected]
• [Metamath] FYI: us.metamath.org is *NOT* vulnerable to CVE-2024-6387 (race condition in sshd) 'David A. Wheeler' via Metamath
  • Re: [Metamath] FYI: us.metamath.org is *NOT* vulnerable to CVE-2024-6387 (race condition in sshd) Jim Kingdon
• [Metamath] Re: Another contribution to Metamath's mmsolitaire project Gino Giotto
  • Re: [Metamath] Re: Another contribution to Metamath's mmsolitaire project Mario Carneiro
  • Re: [Metamath] Re: Another contribution to Metamath's mmsolitaire project [email protected]
  • Re: [Metamath] Re: Another contribution to Metamath's mmsolitaire project Mario Carneiro
• [Metamath] Shortest possible axiom for propositional calculus heiphohmia via Metamath
  • [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus 'Thierry Arnoux' via Metamath
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Mario Carneiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Mario Carneiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Mario Carneiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Gino Giotto
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Steven Nguyen
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Jeff Hoffman
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Steven Nguyen
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus Steven Nguyen
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • AW: [Metamath] Re: Shortest possible axiom for propositional calculus Discher, Samiro
  • Re: [Metamath] Re: Shortest possible axiom for propositional calculus [email protected]
• [Metamath] Metamath proof visualizer with graphs Matthias Vogt
  • Re: [Metamath] Metamath proof visualizer with graphs Mario Carneiro
  • Re: [Metamath] Metamath proof visualizer with graphs Johnathan Mercer
  • AW: [Metamath] Metamath proof visualizer with graphs Discher, Samiro
  • Re: [Metamath] Metamath proof visualizer with graphs Matthias Vogt
  • Re: [Metamath] Metamath proof visualizer with graphs 'David A. Wheeler' via Metamath
  • AW: [Metamath] Metamath proof visualizer with graphs Discher, Samiro
  • Re: [Metamath] Metamath proof visualizer with graphs Matthias Vogt
  • Re: [Metamath] Metamath proof visualizer with graphs 'David A. Wheeler' via Metamath
  • Re: [Metamath] Metamath proof visualizer with graphs 'Thierry Arnoux' via Metamath
• [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 [email protected]
  • Re: [Metamath] Feedback from metakunt, a recent contributor Jim Kingdon
  • Re: [Metamath] Feedback from metakunt, a recent contributor 'Andrew Thompson Thompson' via Metamath
  • Re: [Metamath] Feedback from metakunt, a recent contributor Jim Kingdon
  • Re: [Metamath] Feedback from metakunt, a recent contributor 'Andrew Thompson Thompson' via Metamath
  • [Metamath] Re: Feedback from metakunt, a recent contributor Glauco
• [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 [email protected]
  • [Metamath] Re: Release of pmGenerator 1.2: User-definable systems, and proof minimization challenges [email protected]
• [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 [email protected]
  • 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

• Earlier messages
• Later messages