metamath  

Messages by Thread

• • [Metamath] Re: Formalizing IMO B2.1972 Jon P
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
  • Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
  • Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Formalizing IMO B2.1972 Dirk-Anton Broersen
  • Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
  • Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
• [Metamath] Should we make both discouragement tags mandatory in *OLD and *ALT? Norman Megill
  • Re: [Metamath] Should we make both discouragement tags mandatory in *OLD and *ALT? Thierry Arnoux
  • [Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT? Norman Megill
  • [Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT? Norman Megill
  • [Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT? 'Alexander van der Vekens' via Metamath
• [Metamath] If the humanity disappear 'fl' via Metamath
  • [Metamath] Re: If the humanity disappear vvs
  • [Metamath] Re: If the humanity disappear vvs
  • [Metamath] Re: If the humanity disappear 'fl' via Metamath
  • [Metamath] Re: If the humanity disappear vvs
  • [Metamath] Re: If the humanity disappear 'fl' via Metamath
  • [Metamath] Re: If the humanity disappear vvs
  • Re: [Metamath] Re: If the humanity disappear Sauer, Andrew Jacob
  • Re: [Metamath] Re: If the humanity disappear vvs
  • [Metamath] Re: If the humanity disappear 'fl' via Metamath
  • Re: [Metamath] Re: If the humanity disappear Sauer, Andrew Jacob
• [Metamath] Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.) Ken Kubota
  • [Metamath] Re: Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.) Norman Megill
  • [Metamath] Re: Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.) Norman Megill
• [Metamath] Where is the fashionable mathematics? David A. Wheeler
  • Re: [Metamath] Where is the fashionable mathematics? Jim Kingdon
  • Re: [Metamath] Where is the fashionable mathematics? Raph Levien
  • Re: [Metamath] Where is the fashionable mathematics? Jim Kingdon
  • Re: [Metamath] Metamath Zulip Thierry Arnoux
  • Re: [Metamath] Metamath Zulip savask
  • Re: [Metamath] Metamath Zulip Mario Carneiro
  • Re: [Metamath] Metamath Zulip 'fl' via Metamath
  • [Metamath] Re: Where is the fashionable mathematics? Norman Megill
  • Re: [Metamath] Re: Where is the fashionable mathematics? Mario Carneiro
  • [Metamath] Re: Where is the fashionable mathematics? savask
• [Metamath] Analysis of full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Analysis of full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Analysis of full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Analysis of full 'minimize' run on set.mm David A. Wheeler
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm Glauco
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm 'fl' via Metamath
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm Benoit
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
  • [Metamath] Re: Analysis of full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm Thierry Arnoux
  • Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
• [Metamath] My latest minimize status David A. Wheeler
  • Re: [Metamath] My latest minimize status David A. Wheeler
  • Re: [Metamath] My latest minimize status Norman Megill
  • Re: [Metamath] My latest minimize status David A. Wheeler
  • Re: [Metamath] My latest minimize status 'fl' via Metamath
• [Metamath] recursive function, computablity vs formulae persres
  • Re: [Metamath] recursive function, computablity vs formulae Paul Chapman
  • Re: [Metamath] recursive function, computablity vs formulae Giovanni Mascellani
  • Re: [Metamath] recursive function, computablity vs formulae 'fl' via Metamath
• [Metamath] About Metamath zero (mm0) Olivier Binda
  • [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
  • Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
  • [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
  • Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
  • Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
  • Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
• [Metamath] Re: RFC: Mandatory definitions after constants 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: RFC: Mandatory definitions after constants Mario Carneiro
  • Re: [Metamath] Re: RFC: Mandatory definitions after constants Benoit
  • Re: [Metamath] Re: RFC: Mandatory definitions after constants Mario Carneiro
• [Metamath] Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
  • Re: [Metamath] Riemann-zeta ratio-test rabbit-hole Mario Carneiro
  • Re: [Metamath] Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
  • [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Thomas Brendan Leahy
  • [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
  • Re: [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Mario Carneiro
  • Re: [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
  • Re: [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
• [Metamath] Full 'minimize' run on set.mm Norman Megill
  • [Metamath] Re: Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Benoit
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Benoit
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • [Metamath] Minimize using "dummylink" and "idi" in fourierdlem48? David A. Wheeler
  • Re: [Metamath] Minimize using "dummylink" and "idi" in fourierdlem48? Mario Carneiro
  • Re: [Metamath] Minimize using "dummylink" and "idi" in fourierdlem48? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Minimize using "dummylink" and "idi" in fourierdlem48? Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Full 'minimize' run on set.mm 'fl' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Benoit
  • Re: [Metamath] Full 'minimize' run on set.mm Giovanni Mascellani
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm Giovanni Mascellani
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm Giovanni Mascellani
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm Giovanni Mascellani
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm heiphohmia via Metamath
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Thierry Arnoux
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Breaking up ~ mideulem and ~ footex Thierry Arnoux
  • Re: [Metamath] Breaking up ~ mideulem and ~ footex Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Mario Carneiro
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm David Starner
  • Re: [Metamath] Full 'minimize' run on set.mm David A. Wheeler
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
  • Re: [Metamath] Full 'minimize' run on set.mm Norman Megill
• [Metamath] Are we listening? vvs
  • Re: [Metamath] Are we listening? OlivierBinda
  • Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Ken Kubota
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Norman Megill
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Ken Kubota
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Mario Carneiro
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Ken Kubota
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Mario Carneiro
  • Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening? Ken Kubota

• Later messages