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).<p>[1] <a href="https://cs.nyu.edu/pipermail/fom/2016-January/019441.html" rel="nofollow">https://cs.nyu.edu/pipermail/fom/2016-January/019441.html</a><p>[2] <a href="https://cs.nyu.edu/pipermail/fom/2018-June/021032.html" rel="nofollow">https://cs.nyu.edu/pipermail/fom/2018-June/021032.html</a>
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).<p>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.
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.<p>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.<p>For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics.<p>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.<p>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.<p>All the set theory (and the number theory) can be constructed from these alternative primitive concepts.
Here is a plan to improve proof assistants, and it is based on set theory: <a href="https://www.practal.com" rel="nofollow">https://www.practal.com</a>
Program extraction.<p>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.<p>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.<p>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.
> A set 𝑋 is jaberwocky when for every 𝑥∈𝑋 there exists a bryllyg 𝑈⊆𝑋 and an uffish 𝐾⊆X such that 𝑥∈𝑈 and 𝑈∈𝐾.<p>Anyone know how this relates to Lewis Carrol?