I’ve really been getting into Lean, and these tutorials are fantastic. It’s always interesting to see how many hidden assumptions are made in short and informal mathematical proofs that end up becoming a (very long) sequence of formal transformations when all of the necessary steps are written out explicitly.
My guess is that mathematical research utilizing these systems is probably the future of most of the field (perhaps to the consternation of the old guard). I don’t think it will replace human intuition, but the hope is that it will augment it in ways we didn’t expect or think about. Terence Tao has a great blog post about this, specifically about how proof assistants can improve collaboration.
On another note, these proof systems always prompt me to think about the uncomfortable paradox that underlies mathematics, namely, that even the simplest of axioms cannot be proven “ex nihilo” — we merely trust that a contradiction will never arise (indeed, if the axioms corresponding to the formal system of a sufficiently powerful theory are actually consistent, we cannot prove that fact from within the system itself).
The selection of which axioms (or finite axiomatization) to use is guided by... what exactly then? Centuries of human intuition and not finding a contradiction so far? That doesn’t seem very rigorous. But then if you try to select axioms probabilistically (e.g., via logical induction), you end up with a circular dependency, because the predictions that result are only as rigorous as the axioms underlying the theory of probability itself.
To be clear, I’m not saying anything actual mathematicians haven’t already thought about (or particularly care about that much for their work), but for a layperson, the increasing popularity of these formal proof assistants certainly brings the paradox to the forefront.
The selection of which axioms to use is an interesting topic. Historically, axioms were first used by Hilbert and cie. while trying to progress in set theory. The complexity of the topic naturally led them to formalize their work, and thus arose ZF(C) [1], which later stuck as the de facto basis of modern mathematics.
Later systems, like Univalent Fundations [2] came from some limitations of ZFC and the desire to have a set of axioms that is easier to work with (for e.g. computer proof assistants). The choice of any new systems of axioms is ultimately limited by the scope of what ZFC can do, so as to preserve the past two centuries of mathematical works.
>>> The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.
Then you add in the Brouwer Hilbert mess that still causes challenges with talking about where the a priori assumption of the law of the excluded middle causes real problems with modern computational challenge.
> My guess is that mathematical research utilizing these systems is probably the future of most of the field (perhaps to the consternation of the old guard). ... Terence Tao has a great blog post about this, specifically about how proof assistants can improve collaboration.
Yeah, that was a great blog post. As someone who started in mathematics but ended up in computing, I read it and realized, hang on, he is talking about taking a devops approach to mathematics. It definitely struck me that this is the way of the future: mathematics transformed from almost a humanities-like discipline into an engineered enterprize.
My guess is that mathematical research utilizing these systems is probably the future of most of the field (perhaps to the consternation of the old guard). I don’t think it will replace human intuition, but the hope is that it will augment it in ways we didn’t expect or think about. Terence Tao has a great blog post about this, specifically about how proof assistants can improve collaboration.
On another note, these proof systems always prompt me to think about the uncomfortable paradox that underlies mathematics, namely, that even the simplest of axioms cannot be proven “ex nihilo” — we merely trust that a contradiction will never arise (indeed, if the axioms corresponding to the formal system of a sufficiently powerful theory are actually consistent, we cannot prove that fact from within the system itself).
The selection of which axioms (or finite axiomatization) to use is guided by... what exactly then? Centuries of human intuition and not finding a contradiction so far? That doesn’t seem very rigorous. But then if you try to select axioms probabilistically (e.g., via logical induction), you end up with a circular dependency, because the predictions that result are only as rigorous as the axioms underlying the theory of probability itself.
To be clear, I’m not saying anything actual mathematicians haven’t already thought about (or particularly care about that much for their work), but for a layperson, the increasing popularity of these formal proof assistants certainly brings the paradox to the forefront.