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.
Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.
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).
Correct me if I'm wrong (I may well be), but couldn't one work classically just by sticking to (-1)-truncated types ("mere prepositions") in a HOTT based system, for which LEM is true by default?
Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.
Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.
What makes the cubical approach more powerful? What makes lean weak?
Lean is not weak, it just commits to something called Uniqueness of Identity Proofs (UIP). This is inconsistent with Univalence, a property that cubical type theories have. Necessarily, neither system can express "all of math." So it goes.
Leo chose UIP to get a novel way to get really powerful automation of equality proofs. Leo is very, very good at this; this is his whole shindig. But he had to hack around things a bit in order to get what he wanted. The paper by Bas and his student shows that in cubical, you don't have to hack around things; this automation of equality proofs arises in the natural way.
The gap is not fundamental, and it irritates me when it is attributed to the choice of UIP. The reason Lean is so useful is because the people working on it are good at building automation. The people working on cubical are much more interested in foundations. We need people who are interested in automating cubical; once we get that, the proof assistant that arises from it will be better than anything we have ever seen.
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.
The OP gives a reason, and it's the same reason programs use types. Untyped proofs are usually wrong, like untyped programs.
[1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...
Anyone know how this relates to Lewis Carrol?
[1] https://cs.nyu.edu/pipermail/fom/2016-January/019441.html
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.
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.
