[tlringer]

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.

[throwaway45434]

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

[tlringer]

It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct.

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.

[throwaway45434]

I agree with you that it's not obvious that Lean is the only or best option for formalizing "all" or at least most of mathematics. But I didn't get the impression that Kevin thinks that it's the best tool imaginable but rather the best tool that is currently available.

But that wasn't the point: He's right in that constructive/intuitionistic mathematics is so niche that it can be safely ignored when discussing formalization of the mathematics he and almost every other mathematician or scientist is interested in.

Kevin gets attention because he's an accomplished mathematician who tries to formalize his work, or at least what it's based on. I find it ridiculous to dismiss his opinion the way you do.

[tlringer]

Lean is not classical. I don't know where the idea that Lean is classical is coming from. Lean is constructive. It is consistent with classical axioms, just like Coq is, and just like Cubical is in the propositional fragment. Isabelle/HOL on the other hand is classical, and is quite a natural choice if classical logic is what you want, which is why mathematicians have been using it for decades now.

I know Kevin. He does good work. He also heckled every talk at ITP, including my own, in the middle to express his opinions. I have never met another researcher in my life who does that. Media outlets interview him and not the other 50 years of researchers doing work on proof assistants and using them both for mathematics and for verifying systems. I wrote a whole book about the history of program verification and for sure nobody has ever interviewed me about it. Kevin is loud and bold, that is why his opinions spread like fire. But they are just that, opinions.

[lakecresva]

It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's a constructive and non-constructive version of something, the mathlib people will use whatever's easier or nicer to work with. There's some info here about how Lean does realizability with pervasive use of choice: https://github.com/coq/coq/issues/10871#issuecomment-5466412...

[tlringer]

That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive proof assistants can focus on if they want to reach more mathematicians.

[kmill]

Sort of the official policy is that inside proofs (i.e., terms of types in Prop) constructibility doesn't matter, but inside definitions (i.e., terms of types in Type 0 and above) try to be constructive. For example, it is ok to define a function constructively but with a nonconstructive proof of termination.

LEM is used everywhere because it's actually a theorem. It follows from functional extentionality and the existence of quotient types. https://github.com/leanprover/lean/blob/master/library/init/...

The axiom of choice is an actual axiom, and it too ends up being used everywhere, but mostly to introduce decidable instances to permit things like double negation elimination inside proofs. An illustration: [1] introduces these instances to the file and [2] implicitly uses the instance.

[1] https://github.com/leanprover-community/mathlib/blob/master/... [2] https://github.com/leanprover-community/mathlib/blob/master/...

[tlringer]

I have learned more about Kevin and feel bad for bringing up the heckling thing now. I would ignore that part of what I said.

[withtypes]

Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice.

I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".

[tlringer]

I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men.

Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation.

Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.

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

[JoeCamel]

I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?

[TheAsprngHacker]

UIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same.

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.

[bollu]

UIP is "unicity of identity proofs". I think this will rule proofs where we wish to talk about proofs of equality of two objects. I don't know off the top of my head any math that wants to do such a thing, but I'm far from an expert.

[lakecresva]

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?

[ianandrich]

Are you talking along the lines of the red family of provers?

What makes the cubical approach more powerful? What makes lean weak?

[tlringer]

There is RedPRL, there is also cubical Agda. I think cubical Agda is the best developed so far. It lacks automation. But that is not fundamental, it is thanks to the philosophies of the people involved.

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.

[creata]

Do you have any introductory material on cubical type theory, suitable for the average mathematician? The type theory in Lean feels dead simple to me, but all the online resources on cubical type theory feel impenetrable.

[tlringer]

I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmetho...

But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.

[octoberfranklin]

> all the online resources on cubical type theory feel impenetrable.

Same here.