metamath  

Messages by Thread

• • [Metamath] Re: Formatting section headers 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Formatting section headers Zheng Fan
  • Re: [Metamath] Formatting section headers David A. Wheeler
  • Re: [Metamath] Formatting section headers Benoit
• [Metamath] On Megill's completeness theorem Benoit
  • Re: [Metamath] On Megill's completeness theorem Mario Carneiro
  • Re: [Metamath] On Megill's completeness theorem Benoit
  • Re: [Metamath] On Megill's completeness theorem Mario Carneiro
  • Re: [Metamath] On Megill's completeness theorem Mario Carneiro
  • Re: [Metamath] On Megill's completeness theorem Norman Megill
  • Re: [Metamath] On Megill's completeness theorem Benoit
  • Re: [Metamath] On Megill's completeness theorem Mario Carneiro
• [Metamath] Informal proof of Weak Deduction Theorem vs dedt Gustavo Gonçalves
  • Re: [Metamath] Informal proof of Weak Deduction Theorem vs dedt Mario Carneiro
  • Re: [Metamath] Informal proof of Weak Deduction Theorem vs dedt Mario Carneiro
  • Re: [Metamath] Informal proof of Weak Deduction Theorem vs dedt Benoit
  • Re: [Metamath] Informal proof of Weak Deduction Theorem vs dedt Norman Megill
• [Metamath] Translation to/from other languages [email protected]
  • Re: [Metamath] Translation to/from other languages Mario Carneiro
• [Metamath] How to instantiate a theorem by substituting a wff in it? Philip B.
  • Re: [Metamath] How to instantiate a theorem by substituting a wff in it? Mario Carneiro
• [Metamath] World Logic Day 2021 Norman Megill
• [Metamath] Theorem proving with blocks Ishan Murphy
  • [Metamath] Re: Theorem proving with blocks Mo Ti
  • [Metamath] Re: Theorem proving with blocks [email protected]
• [Metamath] MM0/MM1 tutorial Mario Carneiro
  • [Metamath] Re: MM0/MM1 tutorial Benoit
  • Re: [Metamath] Re: MM0/MM1 tutorial Mario Carneiro
• [Metamath] Metamath Speedrun! Jia Ming
  • Re: [Metamath] Metamath Speedrun! Jim Kingdon
• [Metamath] Recent partial unbundling of ax-7, ax-8, ax-9 Benoit
  • Re: [Metamath] Recent partial unbundling of ax-7, ax-8, ax-9 Mario Carneiro
  • Re: [Metamath] Recent partial unbundling of ax-7, ax-8, ax-9 Benoit
• [Metamath] Preferred representation of a polynomial 'Stanislas Polu' via Metamath
• [Metamath] Proposal for on-going proof minimization Norman Megill
  • [Metamath] Re: Proposal for on-going proof minimization savask
  • [Metamath] Re: Proposal for on-going proof minimization 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Proposal for on-going proof minimization 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Proposal for on-going proof minimization Norman Megill
  • [Metamath] Re: Proposal for on-going proof minimization 'Alexander van der Vekens' via Metamath
  • [Metamath] Recommending proof length limits David A. Wheeler
  • [Metamath] Re: Recommending proof length limits 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Recommending proof length limits Mario Carneiro
  • Re: [Metamath] Recommending proof length limits David A. Wheeler
  • Re: [Metamath] Recommending proof length limits Mario Carneiro
  • RE: [Metamath] Recommending proof length limits Dirk-Anton Broersen
  • Re: [Metamath] Proposal for on-going proof minimization David A. Wheeler
  • Re: [Metamath] Proposal for on-going proof minimization Benoit
  • Re: [Metamath] Proposal for on-going proof minimization 'Alexander van der Vekens' via Metamath
• [Metamath] The EMetamath plugin for Ecplise Thierry Arnoux
  • Re: [Metamath] The EMetamath plugin for Ecplise Jim Kingdon
  • Re: [Metamath] The EMetamath plugin for Ecplise [email protected]
  • Re: [Metamath] The EMetamath plugin for Ecplise David A. Wheeler
  • [Metamath] Re: The EMetamath plugin for Ecplise Glauco
  • Re: [Metamath] Re: The EMetamath plugin for Ecplise Thierry Arnoux
• [Metamath] Visualization of proofs with javascript and SVG Igor Ieskov
  • [Metamath] Re: Visualization of proofs with javascript and SVG Norman Megill
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Paul Chapman
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Jim Kingdon
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Igor Ieskov
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Norman Megill
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Igor Ieskov
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Igor Ieskov
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Benoit
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Norman Megill
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Norman Megill
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Igor Ieskov
  • Re: [Metamath] Re: Visualization of proofs with javascript and SVG Igor Ieskov
  • Re: [Metamath] Visualization of proofs (and important metamath.exe update note) Norman Megill
  • Re: [Metamath] Visualization of proofs (and important metamath.exe update note) Igor Ieskov
  • Re: [Metamath] Visualization of proofs with javascript and SVG Jim Kingdon
• [Metamath] Incorrect definition reference in HTML page for ILE 'wal' Marnix Klooster
  • Re: [Metamath] Incorrect definition reference in HTML page for ILE 'wal' Jim Kingdon
  • [Metamath] Re: Incorrect definition reference in HTML page for ILE 'wal' Norman Megill
  • Re: [Metamath] Re: Incorrect definition reference in HTML page for ILE 'wal' Jim Kingdon
• [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? David A. Wheeler
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? Stef O'Rear
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? David A. Wheeler
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? David A. Wheeler
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? 'ML' via Metamath
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? Stef O'Rear
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? David A. Wheeler
  • Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)? Mario Carneiro
• [Metamath] New community verifier? Mario Carneiro
  • [Metamath] Re: New community verifier? vvs
  • Re: [Metamath] Re: New community verifier? Raph Levien
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? Tom Houlé
  • [Metamath] Re: New community verifier? Glauco
  • [Metamath] Re: New community verifier? vvs
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? vvs
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? vvs
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] Re: New community verifier? Glauco
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? Glauco
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? David A. Wheeler
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] Re: New community verifier? Glauco
  • Re: [Metamath] Re: New community verifier? Glauco
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? savask
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] Re: New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? savask
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Glauco
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Glauco
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Glauco
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Norman Megill
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Zheng Fan
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] Re: New community verifier? Glauco
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? [email protected]
  • Re: [Metamath] New community verifier? David A. Wheeler
  • [Metamath] Re: New community verifier? 'ML' via Metamath
  • Re: [Metamath] Re: New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Jim Kingdon
  • Re: [Metamath] New community verifier? Mario Carneiro
  • Re: [Metamath] New community verifier? Thierry Arnoux
  • Re: [Metamath] New community verifier? Benoit
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? David A. Wheeler
  • Re: [Metamath] New community verifier? David A. Wheeler
• [Metamath] Question from Filip about milpgame proof assistant Norman Megill
• [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) David A. Wheeler
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Jim Kingdon
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) David A. Wheeler
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Benoit
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) David A. Wheeler
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) Mario Carneiro
  • Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else) David A. Wheeler
• [Metamath] Re: A bird's eye view of (fragments of) propositional calculus in set.mm Norman Megill
• [Metamath] Relabeling ~dummylink Benoit
  • Re: [Metamath] Relabeling ~dummylink Jim Kingdon
  • Re: [Metamath] Relabeling ~dummylink Scott Fenton
  • Re: [Metamath] Relabeling ~dummylink Mario Carneiro
• [Metamath] Question about (extra) DVs 'Stanislas Polu' via Metamath
  • [Metamath] Re: Question about (extra) DVs Norman Megill
  • Re: [Metamath] Re: Question about (extra) DVs 'Stanislas Polu' via Metamath
  • [Metamath] Re: Question about (extra) DVs Benoit
• [Metamath] Verifying Disjoint Variable Restrictions 'Alexandre Frechette' via Metamath
  • [Metamath] Re: Verifying Disjoint Variable Restrictions 'Alexandre Frechette' via Metamath
  • Re: [Metamath] Re: Verifying Disjoint Variable Restrictions Mario Carneiro
  • Re: [Metamath] Re: Verifying Disjoint Variable Restrictions 'Alexandre Frechette' via Metamath
  • Re: [Metamath] Re: Verifying Disjoint Variable Restrictions Mario Carneiro
  • Re: [Metamath] Re: Verifying Disjoint Variable Restrictions Norman Megill
• [Metamath] Should I be indenting to the last symbol possible? [email protected]
  • [Metamath] Re: Should I be indenting to the last symbol possible? Norman Megill
• [Metamath] Simple substitution in Metamath 'Alexandre Frechette' via Metamath
  • Re: [Metamath] Simple substitution in Metamath Mario Carneiro
  • Re: [Metamath] Simple substitution in Metamath David A. Wheeler
  • Re: [Metamath] Simple substitution in Metamath David A. Wheeler
  • Re: [Metamath] Simple substitution in Metamath 'Alexandre Frechette' via Metamath
• [Metamath] FYI: Metamath databases, executable, and book are archived as part of the GitHub Arctic Code Vault David A. Wheeler
• [Metamath] Automatic proof verification [email protected]
  • Re: [Metamath] Automatic proof verification David Starner
  • Re: [Metamath] Automatic proof verification [email protected]
  • [Metamath] Re: Automatic proof verification Norman Megill
• [Metamath] GPT-f AITP'20 Presentation 'Stanislas Polu' via Metamath
  • [Metamath] Re: GPT-f AITP'20 Presentation [email protected]
• [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
  • Re: [Metamath] GPT-f paper David A. Wheeler
  • Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
  • Re: [Metamath] GPT-f paper savask
  • Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath

• Earlier messages
• Later messages