You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3.
The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substantial user base of mathematicians somewhat familiar with the subject at hand (i.e., condensed mathematics).
The initial challenge by Peter Scholze was directed at all theorem proving communities. As far as I know, only the Lean community took up the challenge.
(Concerning Lean 4: yes, mathlib will have to be ported. And yes, people are working hard on this. I think that none of the theorem provers so far are ready for wide-scale use in mathematics. And that's why it is important to iterate fast. The Lean community is not afraid of redesigns and large refactors when discovering better approaches.)
You are right, my bad. Taking my words back on that.
A bit more details from the Pierre-Marie Pédrot:
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.
> The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician).
> Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity.
> In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.
This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it.
Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil?
There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.
I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.
>There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.
I think it just takes time to fully move on. And while it's not the fault of the Lean community, when something like the recent quantamagazine article on formalizing mathematics essentially only mentions Coq to call it old and busted in comparison to Lean, that's only going to cause people to hold onto their resentments for longer.
It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.
And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.
It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)
[1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...
[Edit, this comment only replies to the first paragraph of parent. I wrote it before parent was edited.]
It's certainly good to avoid breaking subject reduction even more though ;)
Compare it to porting machine code for one instruction set to another instruction set. This is usually doable in a straightforward manner (maybe with a mild performance penalty). But transpiling idiomatic Java to idiomatic Haskell is nigh impossible.
Luckily, the differences between Lean 3 and Lean 4 are not as large as between Java and Haskell. But still, they have different idioms, different syntax, different features. And this has to be taken care of.
- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.
- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained
About incompatibility: Last time I checked (some 3 or so years ago), Coq was not backwards compatible either, and libraries had to be ported manually with each update. Sadly, as this is the one greatest anti-feature that is currently putting me off proof assistants, but probably it needs some time, and the quickest way to get there is to maximize usage. From what I know about Coq and Lean, I suspect Lean will stabilize faster than Coq does, due to it being more "declarative" (Coq is based too much on complex tactics, which are hard to make stable by design).
It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.
Here's an analogue. It's like saying "Goedel proved that maths was undecidable therefore maths is unusable and you shouldn't prove theorems". The point is that Goedel's observation is of no practical relevance to a modern number theorist and does not provide any kind of obstruction in practice to the kind of things that number theorists think about.
I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break theoretical properties, but instead into examples where checking defeq is inacceptably slow, which remains an issue even when defeq is decidable.
From my understanding CiC is used because it allows using a unified language for proofs, specifications, programs and types, which greatly simplifies the system. For example, in Lean 4, more or less the entire system is built on the same core term language: Proofs, propositions / specifications, programs, tactics (i.e. meta programs), the output of tactics and even Lean 4 itself are all written in that same language, even if they don't always use the same method of computation. In my eyes, for the purposes of writing and checking proofs, CiC is quite complex; but if you want to capture all of the above and have them all checked by the same kernel, CiC seems like a fairly minimal metatheory to do so, even with undecidable type checking.
There are a few other examples but this is the one that immediately sprung to mind. The complexity of CiC is very much about decidable typechecking, it's not fundamental to writing a sound dependently typed proof assistant. And anyone who has actually worked on a kernel for CiC knows that while it is "minimal" compared to what people want to do with it, no efficient kernel is nearly as minimal as something like λP2 with dependent intersections.
That particular paper is from 2016 and the type theory presented there is still lacking a number of features from CIC, with those particular extensions being listed as further research. Work on Lean started in 2013 and the kernel in particular has not been touched in a long time for good reason. Around that time, CIC was already battle-proven with there being popular and well-tested reference implementations to learn from. Since then, all the fancy work has been done on the system surrounding the kernel.
I believe one of the goals at the start was that the kernel should be sufficiently simple and small so that it is easy to ensure that the kernel is correct. Despite the apparent redundant complexity that you suggest, the implementation still seems to be sufficiently simple to reach this goal, as no proof of false that was a result of a kernel bug has been reported yet. CIC being well-tested surely also contributed to that.
Another reason is that, as I understand it, it was not always obvious that Lean would break decidability of defeq. Afaik proof irrelevance was only baked in with Lean 3, while it was an option before that. By that point I don't see much of a reason to rewrite an entire kernel that has worked fine so far.
I also vaguely remember that there were arguments related to performance in favor of the current system (e.g. versus W-types), but I don't really understand these things well enough to make that point with confidence :)
In terms of stuff that do go more or less directly through the kernel, some followup papers to the one I linked discuss how to translate inductive definitions etc. automatically into a form accepted by the simpler kernel, so I am even more confident that this would not present a problem.
MSR funds a single developer. The Lean community consists of at least 30 or so active contributors right now, with many more having contributed in the past. Most folks work in academia. Much of Lean's success is absolutely due to the work of that single developer, but I don't think that the playing field is uneven due to MSR's funding.
[1] https://github.com/coq/coq/issues/10871