Should ZFCbot get trained on random ZFC; random ZFC + library of theorems and conjectures and random combinations of high level maths concepts; or random ZFC plus whatever ChatMathsGPT keeps asking.
None of the above. The “foundations of mathematics” is called that because the field emerged in the context of the “foundational crisis” in the philosophy of mathematics; it does not serve as a practical foundation for math as practiced by mathematicians. The overwhelming majority of mathematicians work informally (which is still very formal by the standards of any other field), and my impression is that those who are interested in formal methods are mostly pursuing constructive/type-theoretic approaches. Lean, for instance, is based on the calculus of inductive constructions: “importing” mathlib into ZFC (without just building a model of CIC within it) would be incredibly difficult.
Lean, for instance, is based on the calculus of inductive constructions: “importing” mathlib into ZFC (without just building a model of CIC within it) would be incredibly difficult.
I just want to mention that Lean’s mathlib focuses on classical rather than constructive mathematics, and accepts routinely the law of excluded middle in proofs.
It focuses on classical rather than constructive mathematics.
Yes, terms in Prop are routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.
None of the above. The “foundations of mathematics” is called that because the field emerged in the context of the “foundational crisis” in the philosophy of mathematics; it does not serve as a practical foundation for math as practiced by mathematicians. The overwhelming majority of mathematicians work informally (which is still very formal by the standards of any other field), and my impression is that those who are interested in formal methods are mostly pursuing constructive/type-theoretic approaches. Lean, for instance, is based on the calculus of inductive constructions: “importing” mathlib into ZFC (without just building a model of CIC within it) would be incredibly difficult.
I just want to mention that Lean’s mathlib focuses on classical rather than constructive mathematics, and accepts routinely the law of excluded middle in proofs.
It focuses on classical rather than constructive mathematics.
Yes, terms in
Propare routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.