metamath  

Messages by Thread

• [Metamath] OpenAI search tool for set.mm theorems Auguste Poiroux
  • Re: [Metamath] OpenAI search tool for set.mm theorems Mario Carneiro
  • Re: [Metamath] OpenAI search tool for set.mm theorems 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI search tool for set.mm theorems Auguste Poiroux
• [Metamath] Re: More proof shortenings from OpenAI's models 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
  • [Metamath] Re: More proof shortenings from OpenAI's models Norman Megill
  • Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
• [Metamath] Perhaps we should create some unshortened "simple examples" David A. Wheeler
  • Re: [Metamath] Perhaps we should create some unshortened "simple examples" 'Stanislas Polu' via Metamath
  • Re: [Metamath] Perhaps we should create some unshortened "simple examples" David A. Wheeler
• [Metamath] Historical works 'fl' via Metamath
• Re: [Metamath] More proof shortenings from OpenAI's models David A. Wheeler
  • Re: [Metamath] More proof shortenings from OpenAI's models 'ookami' via Metamath
  • Re: [Metamath] More proof shortenings from OpenAI's models Glauco
  • Re: [Metamath] More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
• [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift David A. Wheeler
  • Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift Richard Penner
  • Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
  • Re: [Metamath] Frege's Begriffsschrift Norman Megill
  • Re: [Metamath] Frege's Begriffsschrift Norman Megill
  • Re: [Metamath] Frege's Begriffsschrift Richard Penner
• [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath David A. Wheeler
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath David Starner
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath Thierry Arnoux
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
  • Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
  • Re: [Metamath] OpenAI Proof Assistant for Metamath Aleksandras Maliuginas
  • Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
  • Re: [Metamath] OpenAI Proof Assistant for Metamath David A. Wheeler
• [Metamath] MM0 -> MM translation challenges Mario Carneiro
  • [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
  • Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
  • Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
  • Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
  • Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
  • Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
  • Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
  • Re: [Metamath] Re: MM0 -> MM translation challenges Jim Kingdon
  • Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
  • Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• [Metamath] Typo in comment to ~ caov? heiphohmia via Metamath
  • [Metamath] Re: Typo in comment to ~ caov? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Typo in comment to ~ caov? heiphohmia via Metamath
  • Re: [Metamath] Re: Typo in comment to ~ caov? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Typo in comment to ~ caov? Antony Bartlett
  • [Metamath] trying to construct cuberoot of 2 Dirk-Anton Broersen
  • Re: [Metamath] Re: Typo in comment to ~ caov? heiphohmia via Metamath
• [Metamath] Metamath C Mario Carneiro
  • Re: [Metamath] Metamath C Giovanni Mascellani
  • Re: [Metamath] Metamath C OlivierBinda
• [Metamath] Proofs by enumerating cases 'Stanislas Polu' via Metamath
  • Re: [Metamath] Proofs by enumerating cases Mario Carneiro
  • Re: [Metamath] Proofs by enumerating cases 'Stanislas Polu' via Metamath
• Re: [Metamath] (FL) Re: Proposal: Change mmj2's CLI David A. Wheeler
• [Metamath] (FL) tensor algebra Norman Megill
  • Re: [Metamath] (FL) tensor algebra Jim Kingdon
  • [Metamath] Re: (FL) tensor algebra 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: (FL) tensor algebra Norman Megill
  • [Metamath] Re: (FL) tensor algebra 'Alexander van der Vekens' via Metamath
• [Metamath] Proposal: Change mmj2's CLI David A. Wheeler
  • Re: [Metamath] Proposal: Change mmj2's CLI Jim Kingdon
  • Re: [Metamath] Proposal: Change mmj2's CLI Mario Carneiro
  • [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
  • [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI Benoit
  • Re: [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI André L F S Bacci
  • [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI Norman Megill
  • [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
  • Re: [Metamath] (FL) Re: Proposal: Change mmj2's CLI David A. Wheeler
  • [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
  • Re: [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI heiphohmia via Metamath
• [Metamath] (FL) Words, Commons and binomial Norman Megill
• [Metamath] Updated Gource visualization now public! David A. Wheeler
• [Metamath] Re: Calculational rendering of Metamath proofs, using Greasemonkey/Firefox Marnix Klooster
• [Metamath] Final (?) draft Gource visualization of set.mm David A. Wheeler
• [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install 'B. Wilson' via Metamath
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David Starner
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
  • Re: [Metamath] Proposed installation conventions so things will be easier to install 'B. Wilson' via Metamath
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Giovanni Mascellani
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David Starner
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
  • Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) Norman Megill
  • Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) Giovanni Mascellani
  • Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) David A. Wheeler
  • Re: [Metamath] Proposed installation conventions so things will be easier to install Jim Kingdon
  • [Metamath] Re: Proposed installation conventions so things will be easier to install savask
  • Re: [Metamath] Re: Proposed installation conventions so things will be easier to install David A. Wheeler
  • [Metamath] Trisecting an angle Dirk-Anton Broersen
  • Re: [Metamath] Trisecting an angle Jim Kingdon
  • Re: [Metamath] Trisecting an angle Dirk-Anton Broersen
• [Metamath] Moving equality across an implication David Starner
  • [Metamath] Re: Moving equality across an implication 'Alexander van der Vekens' via Metamath
• [Metamath] The conditional operator for propositions (now with a reference) Benoit
  • [Metamath] Re: The conditional operator for propositions (now with a reference) 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: The conditional operator for propositions (now with a reference) Benoit
• [Metamath] Best 2012 date for Eric Schmidt's paper "Reductions in Norman Megill’s axiom system for complex numbers"? David A. Wheeler
• [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
  • Re: [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
  • Re: [Metamath] Last-minute comments on updated Gource visualization? Benoit
  • Re: [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
• [Metamath] FL: Nicod, Sheffer Whitehead and Russell Norman Megill
  • [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Benoit
  • [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Norman Megill
  • [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Norman Megill
• [Metamath] us2.metmath.org Norman Megill
• Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
  • Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
  • Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
  • Re: [Metamath] Packaging Metamath for Linux distros David A. Wheeler
  • Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
  • Re: [Metamath] Packaging Metamath for Linux distros David A. Wheeler
  • Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
  • Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
• [Metamath] FL: ++; binary connectives Norman Megill
  • Re: [Metamath] FL: ++; binary connectives Mario Carneiro
  • [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
  • Re: [Metamath] Re: FL: ++; binary connectives 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: FL: ++; binary connectives Benoit
  • Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: FL: ++; binary connectives Benoit
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
  • Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
  • Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
  • Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
  • Re: [Metamath] Re: FL: ++; binary connectives Benoit
  • Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
  • Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
  • Re: [Metamath] Re: FL: ++; binary connectives Benoit
  • Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
  • Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
  • [Metamath] Re: FL: ++; binary connectives Norman Megill
  • Re: [Metamath] Re: FL: ++; binary connectives Benoit
  • Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
  • Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
• [Metamath] bj-df-if and df-ifp Richard Penner
  • [Metamath] Re: bj-df-if and df-ifp Benoit
  • [Metamath] Re: bj-df-if and df-ifp Richard Penner
  • [Metamath] Re: bj-df-if and df-ifp Benoit
• [Metamath] mmj2 users on Windows processing set.mm: May need to increase memory David A. Wheeler
  • [Metamath] Re: mmj2 users on Windows processing set.mm: May need to increase memory 'Alexander van der Vekens' via Metamath
• [Metamath] Can a floating hypothesis become essential? savask
  • [Metamath] Re: Can a floating hypothesis become essential? Norman Megill
  • [Metamath] Re: Can a floating hypothesis become essential? savask
  • [Metamath] Re: Can a floating hypothesis become essential? Norman Megill
• [Metamath] New contributions David Starner
  • Re: [Metamath] New contributions Jim Kingdon
  • Re: [Metamath] New contributions 'Stanislas Polu' via Metamath
  • [Metamath] Re: New contributions Jon P
• [Metamath] Denoting morphisms in set.mm Benoit
  • [Metamath] Re: Denoting morphisms in set.mm Norman Megill
  • [Metamath] Re: Denoting morphisms in set.mm Norman Megill

• Earlier messages
• Later messages