The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. The actual question makes more sense because the one on HN suggests that proof assistants exclusively formalize mathematics in dependent type theory (rather than set theory) which is not true. In fact, some proof assistants use dependent type theory (LEAN), some use simple type theory (Isabelle/HOL), some use simple type theory to encode untyped set theory (Isabelle/ZF), some implement kind of "soft typing" on top of untyped set theory (Mizar) and some are completely generic and can encode all of the above (Metamath).
As for the question why type theory seems to be more popular in formalization of mathematics recently than set theory Jeremy Avigad wrote a rare compelling explanation [1] of why this is the case. I personally prefer the opinion of Lawrence Paulson [2], the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently).
> The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here.
It's too long for HN, OP presumably reworded to fit. If you have a better suggestion one of the mods might see and change it, I think OP's chance to edit it has passed though.
The idea of Lean being suitable for all of math is sensationalist and Kevin knows it. Lean being committed to UIP already rules out many kinds of mathematics. Furthermore, the kind of automation possible in Lean is also possible in univalent theorem provers with the right implementation (e-graphs). They are actually easier in cubical than in Lean (see the 2 pager by Bas Spitters and his masters student).
The difference is that no cubical proof assistant has been implemented by Leo de Moura. Get Leo de Moura to implement cubical, and you will have a proof assistant more powerful than you could ever imagine, built on extremely satisfying foundations.
At least 99% of all mathematicians in academia work with classical logic only, and a good fraction hasn't even heard of anything else. So yeah, Lean might not be suitable for some of the remaining 1%, but that doesn't make Kevin's claim "sensationalist".
Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you tried to get them to used cubical Lean (Lean 2 by the way implemented HoTT ideas) and give up classical logic.
The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing.
Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?
Slightly off-topic, but in any mathematical theory concerning a certain restricted domain and also in any theory attempting to cover the entire mathematics there are many possible choices for the primitive concepts and rules.
In most cases it is not possible to have an objective criterion for deciding which is the best choice, so the choice remains based on personal preferences.
For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics.
I have always believed that it is more convenient to view the sets not as primitives, but as classes of equivalence of the ordered sequences, which in turn are constructed from ordered pairs, which are a primitive concept.
So instead of using set theory as a base, I believe it to be more convenient to start from some primitives that include some of the concepts and operations on which LISP was also based, plus some definitions, which normally are introduced using sets, modified to use ordered sequences instead.
All the set theory (and the number theory) can be constructed from these alternative primitive concepts.
In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and always halts, returning a value of type B. Moreover if you prove some property about proofs that A implies B, you've also proved the corresponding proposition about programs.
This means your proofs get to deal with programs directly, rather than having to formalize them as something like Turing machines whose tapes are set-theoretic encodings of lists of integers. It's excruciatingly painful to write non-hand-wavy proofs of anything that way. Hand-wavy proofs that can't be machine-checked aren't so bad of course; complexity theory folks have been doing that for decades.
If you aren't proving things about programs or homotopy then there really aren't any obvious reasons to prefer dependent type theory. I say this as somebody who loves programming with dependent types. But I'm being honest here, and I wish more people in the mechanized mathematics world would be honest about this.
[+] [-] robinzfc|5 years ago|reply
[1] https://cs.nyu.edu/pipermail/fom/2016-January/019441.html
[2] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html
[+] [-] OJFord|5 years ago|reply
It's too long for HN, OP presumably reworded to fit. If you have a better suggestion one of the mods might see and change it, I think OP's chance to edit it has passed though.
[+] [-] tlringer|5 years ago|reply
The difference is that no cubical proof assistant has been implemented by Leo de Moura. Get Leo de Moura to implement cubical, and you will have a proof assistant more powerful than you could ever imagine, built on extremely satisfying foundations.
[+] [-] throwaway45434|5 years ago|reply
[+] [-] voxl|5 years ago|reply
The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing.
Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
[+] [-] JoeCamel|5 years ago|reply
[+] [-] lakecresva|5 years ago|reply
[+] [-] ianandrich|5 years ago|reply
What makes the cubical approach more powerful? What makes lean weak?
[+] [-] adrian_b|5 years ago|reply
In most cases it is not possible to have an objective criterion for deciding which is the best choice, so the choice remains based on personal preferences.
For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics.
I have always believed that it is more convenient to view the sets not as primitives, but as classes of equivalence of the ordered sequences, which in turn are constructed from ordered pairs, which are a primitive concept.
So instead of using set theory as a base, I believe it to be more convenient to start from some primitives that include some of the concepts and operations on which LISP was also based, plus some definitions, which normally are introduced using sets, modified to use ordered sequences instead.
All the set theory (and the number theory) can be constructed from these alternative primitive concepts.
[+] [-] devit|5 years ago|reply
[+] [-] auggierose|5 years ago|reply
[+] [-] octoberfranklin|5 years ago|reply
In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and always halts, returning a value of type B. Moreover if you prove some property about proofs that A implies B, you've also proved the corresponding proposition about programs.
This means your proofs get to deal with programs directly, rather than having to formalize them as something like Turing machines whose tapes are set-theoretic encodings of lists of integers. It's excruciatingly painful to write non-hand-wavy proofs of anything that way. Hand-wavy proofs that can't be machine-checked aren't so bad of course; complexity theory folks have been doing that for decades.
If you aren't proving things about programs or homotopy then there really aren't any obvious reasons to prefer dependent type theory. I say this as somebody who loves programming with dependent types. But I'm being honest here, and I wish more people in the mechanized mathematics world would be honest about this.
[+] [-] alisonkisk|5 years ago|reply
The OP gives a reason, and it's the same reason programs use types. Untyped proofs are usually wrong, like untyped programs.
[+] [-] jakear|5 years ago|reply
Anyone know how this relates to Lewis Carrol?
[+] [-] creata|5 years ago|reply
https://en.wikipedia.org/wiki/Jabberwocky
[+] [-] pfortuny|5 years ago|reply