[voxl]

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).

[hejsansvejsan]

I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/lib...

[zozbot234]

Proving "classical" propositions in an intuitionistic system is trivial. Intuitionistic logic can be viewed as an extension of classical logic with new "constructive OR" and "constructive EXISTS" operators. The classical operators are recovered via negation: NOT (NOT a AND NOT b) is classical OR, whilst NOT FORALL x (NOT p) is a classical existential quantifier.

[logicchains]

>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?

[hejsansvejsan]

LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.

[tlringer]

Lean isn't classical.

Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.