metamath  

Messages by Thread

• • Re: [Metamath] checkmm ported to TypeScript Antony Bartlett
  • Re: [Metamath] checkmm ported to TypeScript David A. Wheeler
• [Metamath] How should I approach comment parsing? 'Philip White' via Metamath
  • [Metamath] Re: How should I approach comment parsing? Benoit
  • Re: [Metamath] Re: How should I approach comment parsing? Mario Carneiro
  • Re: [Metamath] Re: How should I approach comment parsing? 'Philip White' via Metamath
  • Re: [Metamath] Re: How should I approach comment parsing? Mario Carneiro
  • Re: [Metamath] Re: How should I approach comment parsing? 'Philip White' via Metamath
  • Re: [Metamath] Re: How should I approach comment parsing? Mario Carneiro
• [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Antony Bartlett
  • Re: [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Antony Bartlett
  • Re: [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Thierry Arnoux
  • Re: [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Jon P
  • Re: [Metamath] Lessons from Metamath Mario Carneiro
  • Re: [Metamath] Lessons from Metamath Jon P
• [Metamath] Re: mmverify.py bug Glauco
  • Re: [Metamath] Re: mmverify.py bug Mario Carneiro
  • Re: [Metamath] Re: mmverify.py bug Glauco
  • Re: [Metamath] Re: mmverify.py bug Jim Kingdon
  • Re: [Metamath] Re: mmverify.py bug Benoit
  • Re: [Metamath] Re: mmverify.py bug Antony Bartlett
  • Re: [Metamath] Re: mmverify.py bug Glauco
  • Re: [Metamath] Re: mmverify.py bug Antony Bartlett
  • Re: [Metamath] Re: mmverify.py bug Benoit
• [Metamath] Iowa Type Theory Commute Podcast Thierry Arnoux
• [Metamath] What does Z mean in compressed proofs? 'Philip White' via Metamath
  • Re: [Metamath] What does Z mean in compressed proofs? Mario Carneiro
  • Re: [Metamath] What does Z mean in compressed proofs? Benoit
  • Re: [Metamath] What does Z mean in compressed proofs? 'Philip White' via Metamath
  • Re: [Metamath] What does Z mean in compressed proofs? Benoit
  • Re: [Metamath] What does Z mean in compressed proofs? 'Philip White' via Metamath
• [Metamath] review on iset.mm seq theorems Jim Kingdon
  • [Metamath] Re: review on iset.mm seq theorems 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: review on iset.mm seq theorems Jim Kingdon
• [Metamath] Travis CI webhooks uninstalled Mario Carneiro
  • Re: [Metamath] Travis CI webhooks uninstalled David A. Wheeler
• [Metamath] Kunen's inconsistency axiom-free proof on Metamath Thierry Arnoux
• [Metamath] Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. Jim Kingdon
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. Mario Carneiro
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. Mázsa Péter
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suffix "t" for theorems in closed form. Mázsa Péter
• [Metamath] Mapping Metamath predicate logic to traditional predicate logic Andrew Lubrino
  • Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic Jim Kingdon
  • Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic Andrew Lubrino
  • Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic Jim Kingdon
  • Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic Thierry Arnoux
• [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? David A. Wheeler
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Scott Fenton
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Jim Kingdon
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Cris Perdue
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Mingli Yuan
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Mázsa Péter
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Cris Perdue
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Mázsa Péter
  • [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Mázsa Péter
  • Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org? Cris Perdue
• [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) Benoit
  • Re: [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) Thierry Arnoux
  • Re: [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) David A. Wheeler
  • Re: [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) Mario Carneiro
  • Re: [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) David A. Wheeler
  • Re: [Metamath] Independence questions in set.mm (partial independence of ax-11 and ax-13) Benoit
• [Metamath] A demo to ease mmj2 installation by installer Mingli Yuan
  • [Metamath] Re: A demo to ease mmj2 installation by installer Mingli Yuan
  • [Metamath] Re: A demo to ease mmj2 installation by installer Mingli Yuan
  • Re: [Metamath] Re: A demo to ease mmj2 installation by installer Thierry Arnoux
  • Re: [Metamath] Re: A demo to ease mmj2 installation by installer Mingli Yuan
  • Re: [Metamath] Re: A demo to ease mmj2 installation by installer Thierry Arnoux
• [Metamath] mmj2 and linux mario
  • Re: [Metamath] mmj2 and linux Thierry Arnoux
  • Re: [Metamath] mmj2 and linux mario
• [Metamath] mmj2.zip and Linux mario
• [Metamath] LaTeX rendering mario
  • Re: [Metamath] LaTeX rendering Thierry Arnoux
  • Re: [Metamath] LaTeX rendering mario
• [Metamath] Deleting stale merged branches on 19th February Benoit
• [Metamath] Answer to "Why are my branches getting deleted when someone merges my pull request?" Jim Kingdon
• [Metamath] CI Checks didn't kick in Glauco
  • Re: [Metamath] CI Checks didn't kick in Jim Kingdon
• [Metamath] How to express a quadratic form over a vector space Mingli Yuan
  • [Metamath] Re: How to express a quadratic form over a vector space 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: How to express a quadratic form over a vector space vvs
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mingli Yuan
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mario Carneiro
  • Re: [Metamath] Re: How to express a quadratic form over a vector space 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: How to express a quadratic form over a vector space vvs
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mario Carneiro
  • Re: [Metamath] Re: How to express a quadratic form over a vector space vvs
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mario Carneiro
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Jim Kingdon
  • Re: [Metamath] Re: How to express a quadratic form over a vector space vvs
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mingli Yuan
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Benoit
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mingli Yuan
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Benoit
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Thierry Arnoux
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Mingli Yuan
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Benoit
  • Re: [Metamath] Re: How to express a quadratic form over a vector space Thierry Arnoux
  • Re: [Metamath] How to express a quadratic form over a vector space Thierry Arnoux
  • Re: [Metamath] How to express a quadratic form over a vector space 'Alexander van der Vekens' via Metamath
• [Metamath] Metamath vs Mizar for someone new to abstract math Andrew Lubrino
  • Re: [Metamath] Metamath vs Mizar for someone new to abstract math Mario Carneiro
  • [Metamath] Re: Metamath vs Mizar for someone new to abstract math vvs
  • Re: [Metamath] Re: Metamath vs Mizar for someone new to abstract math Andrew Lubrino
  • Re: [Metamath] Re: Metamath vs Mizar for someone new to abstract math Jim Kingdon
  • Re: [Metamath] Re: Metamath vs Mizar for someone new to abstract math vvs
  • Re: [Metamath] Re: Metamath vs Mizar for someone new to abstract math vvs
• [Metamath] New markup checks Mario Carneiro
  • [Metamath] Re: New markup checks Mario Carneiro
  • Re: [Metamath] Re: New markup checks Mázsa Péter
  • Re: [Metamath] Re: New markup checks Mario Carneiro
  • Re: [Metamath] Re: New markup checks Mario Carneiro
  • Re: [Metamath] Re: New markup checks Jim Kingdon
  • Re: [Metamath] New markup checks David A. Wheeler
  • Re: [Metamath] Re: New markup checks Mázsa Péter
  • Re: [Metamath] Re: New markup checks 'Alexander van der Vekens' via Metamath
  • [Metamath] New markup checks Mázsa Péter
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Mázsa Péter
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] New markup checks Benoit
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Benoit
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Mario Carneiro
  • Re: [Metamath] New markup checks Benoit
  • Re: [Metamath] New markup checks Mario Carneiro
  • [Metamath] Re: New markup checks 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: New markup checks Mario Carneiro
• [Metamath] Tweaks to website generation - now with more files David A. Wheeler
• [Metamath] mm-web-rs server support Mario Carneiro
  • Re: [Metamath] mm-web-rs server support Thierry Arnoux
  • [Metamath] Re: mm-web-rs server support Mario Carneiro
  • [Metamath] Re: mm-web-rs server support Mario Carneiro
• [Metamath] Proposal: Move metamath-knife into the "metamath" organization David A. Wheeler
  • [Metamath] Re: Proposal: Move metamath-knife into the "metamath" organization Benoit
  • Re: [Metamath] Re: Proposal: Move metamath-knife into the "metamath" organization Jim Kingdon
  • Re: [Metamath] Proposal: Move metamath-knife into the "metamath" organization David A. Wheeler
• [Metamath] Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Glauco
  • [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Benoit
  • [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Benoit
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Mario Carneiro
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Benoit
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Mario Carneiro
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Benoit
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Mario Carneiro
  • Re: [Metamath] Re: Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences) Benoit
• [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
  • [Metamath] Re: Big progress on metamath.org and us2.metamath.org Glauco
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org Jim Kingdon
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org Mingli Yuan
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org 'ookami' via Metamath
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Big progress on metamath.org and us2.metamath.org Jim Kingdon
  • [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems David A. Wheeler
  • [Metamath] Re: us2.metamath.org regenerated! Let me know ASAP of any serious problems 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: us2.metamath.org regenerated! Let me know ASAP of any serious problems 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems David A. Wheeler
  • Re: [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems Benoit
  • Re: [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems 'roger witte' via Metamath
• Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Jim Kingdon
  • Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Mázsa Péter
  • Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Thierry Arnoux
  • Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Mázsa Péter
• [Metamath] Metamath website Thierry Arnoux
  • Re: [Metamath] Metamath website David A. Wheeler
  • Re: [Metamath] Metamath website Scott Fenton
  • Re: [Metamath] Metamath website Thierry Arnoux
  • [Metamath] Re: Metamath website Glauco
  • [Metamath] Re: Metamath website Benoit
  • Re: [Metamath] Re: Metamath website Thierry Arnoux
  • Re: [Metamath] Re: Metamath website Benoit
  • Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Metamath website Jim Kingdon
  • Re: [Metamath] Re: Metamath website Thierry Arnoux
  • Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Metamath website Benoit
  • Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath

• Earlier messages
• Later messages