Stack Overflow Question

Asked by Timothy Chow · Score: 49 Tags: set-theory, type-theory, proof-assistants source

Question

Three years ago, I gave an informal talk to my colleagues, suggesting that we were living in the Dumey microsecond when it would still be possible for the mathematical community to throw its weight behind the proof assistant of its choice. Lean already had a lot of momentum because of Kevin Buzzard's Xena Project and Peter Scholze's Liquid Tensor Experiment, but at the time I gave my talk, Terry Tao had not yet taught himself Lean, and the conversion of Mathlib from version 3 to version 4 had just barely been completed. Similarly, the Lean FRO has just barely been launched. Lean did not yet seem as inevitable as it seems today. My question is: Are there any prospects for any organization to seriously support an alternative to Lean? To make the question more concrete, let me suggest Metamath as a candidate. (To be clear, I personally have no vested interest in Metamath or any other specific theorem prover.) I see two things going for Metamath. One of the primary reasons the mathematical community is interested in interactive theorem provers (ITPs) is that they provide a way to validate whether AI-generated proofs (or complicated human proofs, for that matter) are formally correct. As recent events have demonstrated, Lean is not immune to soundness bugs, and finding obscure soundness bugs is the forte of AI. Because of Mario Carneiro's work on Metamath Zero, the assurance of correctness would be significantly higher if we were to use Metamath. Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean and other leading candidates (e.g., Rocq, Agda), as eloquently articulated by James Hanson's recent MO post. Again, I'm not wedded to Metamath; Mizar and Isabelle/ZF are also leading candidates for a set-theoretic ITP (though they do not enjoy a counterpart of Metamath Zero). I am concerned, however, that much of the popularity of Lean can be traced to the fact that a few prominent people happen to have picked it and given it a high profile, not necessarily because it's objectively the best ITP for the job that we want done. The biggest argument in favor of Lean, in my mind, is Mathlib. Replicating Mathlib for any other ITP would, until recently, have seemed completely infeasible in practice. However, given how good AI models have become at writing formal mathematics, I think that it is no longer absurd to contemplate building an analogous library for some other ITP. I'm well aware of the risks of vibe-coded libraries; AI-generated Lean code is currently not high enough quality for Mathlib, and similarly we should not expect AI-generated Metamath code to be as good as Mathlib either. But I don't think we should dismiss the possibility for an alternative to Lean out of hand. Let me also say that I am not advocating ditching Lean. It does have many excellent qualities, and the Lean community is a wonderful community that I don't wish to see destroyed. I am, however, suggesting that having a viable alternative ITP that has higher assurance of soundness and that is based on set theory would be a good thing for the mathematical community as a whole. But this would require some kind of institutional support, and I don't know where that would come from. EDIT: I normally don't bother with disclaimers, taking it for granted that all opinions I express on MO are on my own, but in this particular case, since I work for a U.S. government contractor, perhaps I should state explicitly that I am not aware of anyone in any official government capacity who is dissatisfied with Lean or wants an alternative. Nobody acted on my talk three years ago, and I don't expect anyone to act on my opinions now, either. :-)

Comments

David Roberts (11): I will play devil's advocate, and say that Metamath plays into concerns one might have with the material set theory philosophy. I likewise have no vested interest in any particular theorem prover, it's just that (in my opinion) bringing up philosophical preferences should be secondary to the capability of the proof assistant. Since Metamath can handle arbitrary mathematics (via ZFC and friends), then fine, the question becomes one of usability, which is a different kind of question (technical support, social inertia, investment in development of tooling etc). Same with type-theory-based ones
Julia M. Himmel (10): A proof assistant is not just a proof-checking kernel and a mathematical library. Beside the kernel, the Lean distribution contains a frontend including a parallel and incremental elaborator/tactic framework/tactics/typeclasses, numerous frontend conveniences (like a linting framework), tooling (language server, package manager, etc.), documentation (and a documentation authoring tool), a compiler, and so on. The decision which proof assistant to use should take all of these into account, and perhaps there are cheaper options to increase confidence in proofs than switching entirely.
James E Hanson (10): I believe that the amount of community effort that has been put into Mathlib and related tooling could have built a better proof assistant for pure mathematics by now. Aside from any questions about foundations, Lean has a lot of design decisions that lead to bad UX and poor user-facing performance (i.e., Lean is noticeably sluggish while you are using it on typical hardware).
Jochen Glueck (13): "but at the time [...] Terry Tao had not yet taught himself Lean [...]" I have to say that I find this comment quite alarming. Without any offence intended towards Tao and with all due respect to his contributions to mathematics - but if it is indeed the case that the adaptation of a particular technology throughout mathematics depends so heavily on whether one particularly famous mathematician uses this technology at a particular point in time, then we should really start reconsidering the group dynamics in the math community.
Yemon Choi (9): @JochenGlueck "'I'm not convinced that this dependence on the opinions and actions of one or few specific people is really so strong in reality" - sadly, as an older mathematician who was there in the early days of Internet Personality-Mathematicians, I fear there has always been quite a strong dependence / herd instinct in the dynamics of Online Mathematicians, with people taking their cues from people taking their cues from acolytes of prophets. This goes beyond the topic of Timothy's original post/question.

Answers (7)

Jacques Carette — Score: 34

We are "stuck with Lean" as much as we were "stuck with Internet Explorer". LaTeX, on the other hand, is a much more perplexing example of something we are "stuck with". (Yes, many competitors have existed, and there's even typst rising rapidly now.) And yet. The tools we use are a sociological phenomenon. The main reason the question arises is that mathematicians have tried really hard to ignore such things (i.e. the human factor of mathematics) and pretend that they live in a purely objective world -- even though there are obvious trends and fads in mathematics.

Timothy Chow (3): Are there any prospects for any organization to seriously support an alternative to Lean?

mlk (10): We were never seriously stuck with Internet Explorer. But the internet is definitely stuck with html and javascript (respectively languages that have a similar enough structure to be converted into those). In this context, we can easily replace the lean kernel or slightly alter syntax and notation into something that converts (getting rid of similar but different unicode symbols like ⟨ and < would be trivial and a step forward). But regarding the question, changing from type theory to something else is not just a social question, it means discarding mathlib and all that is built on it.

Jacques Carette (3): @TimothyChow There's Mikan and Jon Sterling's Pterodactyl project, as just two examples of things that could, in time, be real competitors. We're at the "IE rising to crush everyone else" stage, not even at the crest. Lots of time before we're on the other side.

James E Hanson (4): Internet Explorer is not a good metaphor for the situation with Lean. It's not very difficult to switch web browsers and it's something you can do as an individual. Moving a whole proof assistant community and ecosystem is a monumental task by comparison.

James_pic (2): Whilst a user can switch web browsers, if you did so circa 2003, you would find that many web sites were broken, because web developers generally targetted Internet Explorer due to its ubiquity, and its then-poor standards compliance meant that building a web site that looked right in both IE and its competitors was tricky. There was a network effect, even if users and developers would not have considered themselves a community.

James E Hanson — Score: 15

I have a lot of thoughts about this topic and about what a good proof assistant for pure mathematics would look like, most of which don't fit the scope of this question, but I'd like to respond to both your actual question and what I see as an implicit assumption in your question. Your primary question is a little bit difficult to answer because it depends on what 'seriously' means. Is it merely sufficient for the organization providing the alternative to be serious, or does it need to be a meaningfully viable alternative in the sense of attracting an active community? If intent is sufficient, then Prove-It (which is in part developed by researchers at Sandia National Laboratories) is already a positive answer. If you also require some amount of actual activity with the proof assistant, then Mizar might qualify. Let me know if I'm wrong, but I think your question is really intended to be more like 'could an organization support an alternative to Lean that captures a meaningful mind share among mathematicians?' User experience and money I think that a successful alternative is possible, but I think foundations are not really the operant issue. Part of the reason Lean took off is that it had enough money behind it to have better (although, I still maintain, meaningfully bad) user experience than the other major offerings. Annoying foundational considerations do bubble up to the user experience of working with a proof assistant (even in the context of type theory, despite what some people seem to think), but the majority of the usability of a proof assistant has to do with the existence of well-designed libraries and more pedestrian user experience issues like how annoying it is to install, how responsive it is in the editor, good autocomplete, good tutorials or other on-boarding, etc. I said in a comment on your question that the amount of community effort that has been put into the Mathlib ecosystem could have built a better pure math proof assistant, but I think I misphrased that. At some scale you really need some kind of institutional (and therefore monetary) support for this kind of project. (Although Mathlib does have institutional support separate from Lean these days, so my comment doesn't overstep if you include this in 'community effort'.) For example, the Lean FRO also hosts an online Lean editor. This makes it easy to dabble in Lean. (I've heard that some people do all of their Lean work in that web editor.) But the Lean frontend is probably a little bit too bloated to run smoothly in-browser, so when you use this website, the Lean FRO runs a copy of Lean on their server for free. This costs money. Someone is certainly going to get mad at me for saying this, but Isabelle is the only other major proof assistant that in my opinion has made a reasonable effort towards good user experience. That said, their answer (a pre-packaged modified version of jEdit) is by modern standards a bit clunky and dated. I personally (for accessibility reasons) was annoyed by the lack of compatible dark mode support in jEdit, for instance. Beyond this, the formal system of Isabelle/HOL itself suffers from things like a frankly confusing object theory/metatheory distinction that the user is supposed to be shielded from but is nevertheless exposed to often (at least in my experience). Isabelle has a VSCode plugin now, but it seemed to lack polish the last time I looked at it. As far as I can tell, Isabelle doesn't have full-time developers whose whole job is building and maintaining the program, which Lean does. Good full-time developers, again, cost a lot of money. So I feel like this makes the case that money and a full-time development team are pretty essential for building a proof assistant with good, well-maintained user experience. I think that the most plausible structure for such a project would be something similar to the Lean FRO, CoCalc, or Overleaf, an organization focused explicitly on developing a proof assistant for mathematics rather than software development. This could be bankrolled by an existing organization, sure, but I don't think just giving a couple of individual academics grants would be enough. Foundations As you mention in your question, Lean (i.e., the "truth machine" as it has been eye-rollingly dubbed recently) just had a widely publicized kernel soundness bug. The soundness issue involved a feature of Lean that Mario Carneiro's proof of the consistency of the idealized type theory of Lean did not cover (i.e., nested inductive types). Nevertheless, I'm not sure I actually think this is a case for basing a proof assistant on set theory in particular, at least not in a user-facing way. The idea that basing a proof assistant on set theory is the right solution to this issue seems to be an implicit assumption of your question. More broadly, there's a deeper implicit assumption in this whole discourse that proof assistants should be primarily judged on the basis of their foundational systems. To me, thinking about proof assistants in a foundational way, building the user experience from the ground up, is fundamentally wrongheaded. My ideal actually-for-mathematicians proof assistant would be built from the top down. (I think you could do this while still building a soundness architecture that compiles down to something an extremely minimal Metamath-like kernel could check.) For example, Mathlib's category theory library is notoriously awful to use because it runs into all this obnoxious bureaucracy involving managing definitional equality, universes, transport, coherence, and typeclass inference. (Consider for example, the mathematically trivial bookkeeping lemma CategoryTheory.shiftFunctorAdd'_assoc, whose theorem statement is so complicated it contains two inline proof scripts.) Having a smooth user experience for category theory would be a fundamental design goal of my ideal proof assistant, because category theory is a fundamental tool in many parts of mathematics. This would be important enough to potentially motivate very low-level changes to the implementation of the system. But I also wouldn't use categorical foundations because (and, again, someone is going to get mad at me for saying this), categorical foundations are actually pretty bad and difficult to use in practice. Foundationalism makes sense if your goal is industrially paranoid rigor or if your goal is to philosophically ground the semantics of mathematics or to prove metamathematical unprovability results; it doesn't make sense as a UX organizational principle if your goal is to actually do mathematics on a computer.

Timothy Chow (0): To clarify: I suggested Metamath mainly because MM0 is the closest thing we currently have to the (unattainable) goal of absolute certainty. I'm not saying that I expect a set-theoretic foundation to solve all our problems so that we can ditch Lean (I explicitly rejected ditching Lean). That said, in my dream world with two leading candidates, one would be type-theoretic and the other would be set-theoretic, because I think we would learn a lot from the experience. Yes, ideally, foundational niceties should not be "user-facing" but in practice I think some amount of "leakage" is hard to avoid.

Ricky — Score: 11

Disclosure: I am a mathlib maintainer so I am surely biased towards Lean and mathlib. Anyone is free to choose the proof assistant they prefer, the one that works best for them. Of course, there are practical considerations to take into account. Are Lean and mathlib the only practical choice for formalize modern mathematics? I don't think so, but there advantages, so at the end of day it's really about choosing what fits better your need. Lean is the best one for me, but it's not perfect. No software is perfect and no software will last forever, so I don't think we are stuck at all. It's true that currently most mathematicians (that use a proof assistant) use Lean, and this is because, I think, it works better in practice most of the time, and the benefits outweigh the drawbacks in a lot of cases. The community would surely benefit from people using other proofs assistants, but convincing mathematicians in doing so is basically an "open problem". Concerning the verification of proofs generated by AI I think the situation is similar. There is no perfect solution, and at end everything on what is your goal: do you want just an oracle or do you want to understand the proof? Lean seems to provide a reasonable compromise between this two. It offers an high degree of confidence (again, not absolute confidence, I know) and if the proof does not deviate too much from mathlib is usually possible to understand it. So at the end I think we are not really stuck, but it will take quite a lot of time and effort to have other options (and I really hope this will happen!).

Timothy Chow (1): Are there any prospects for any organization to seriously support an alternative to Lean?

Ricky (4): Rocq is already supported (very seriously) by INRIA. But you should ask this question to people working with other proof assistants, not to a Lean person!

mathworker21 (0): Does it offer a high degree of confidence w.r.t. AI solutions? Wouldn't AI quickly and consistently exploit any bug that exists?

Ricky (1): Both Lean and Rocq offer a high degree of confidence. If you mean "an absolute certainty" I am afraid that this is impossible. Like it's impossible to be sure that there are no serious errors in the mathematical literature.

Timothy Chow (1): @mathworker21 Again, if you're not familiar with Metamath Zero, I recommend you look into it. As Ricky says, absolute certainty is impossible, but I think Metamath Zero currently comes the closest.

Lawrence Paulson — Score: 8

Let's generalize your question. Are we stuck with dependent types? I hope not. There are several problems with dependent types. They require proof objects, which waste large amounts of memory. And really for nothing. They require a large and complex kernel, leading to soundness errors. They don't even work: i=j does not guarantee that types T(i) and T(j) are the same. This has led to proof developments and even entire libraries being thrown away, going right back to the Coq era. The amount of mathematics done in Isabelle/HOL does not come close to the amount that has been done in Lean. But there is quite a bit: see the output of one single project. You should at least give it a try before complaining that you are stuck with Lean. [edited to insert links]

Jean Abou Samra (1): Regarding (1), if you have a definitionally proof-irrelevant sort of propositions (like Lean's Prop, Agda or Mikan's Prop, or Rocq's SProp), what would prevent you from never building proof terms for proofs in that sort (except maybe displaying things to the user, which you don't need for batch checking)?

Jean Abou Samra (4): Regarding (2), a full toy implementation of MLTT fits in a couple thousands of lines. It is true that no existing major implementation has a very simple kernel, but the major implementations also try to support "convenience" features. Also, few people may be aware but weak type theory (i.e., type theory without definitional equality) is a thing and implementing it would likely cut down the complexity of type checking a lot. I just don't think the design space of implementing type theory is well-explored enough to make definitive statements like "dependent types require a complex kernel".

Lawrence Paulson (0): Well, there's AUTOMATH, which truly is minimalistic. But who's going to use that?

Michael Bächtold (1): Could you elaborate on 3.?

Anatole Dedecker — Score: 8

Another answer from another Mathlib maintainer, with a potentially different view. I don't think it's possible to answer your question without knowing what you want to do with your proof assistant? I will answer based on my reasons to play with proof assistants, but they will probably not align with yours. I'm maybe an outlier in the Lean mathematical community, but the very point of my involvement with Lean is maintaining and contributing to Mathlib, which I envision as a (very imperfect) modern evolution of Bourbaki. Because I was lucky to learn Lean in my first year of undergrad, Mathlib was a wonderful resource throughout my studies (both in the form of reading formalized material, and contributing yet un-formalized material), and I hope that more people will be able to benefit from it in the way I did. From this point of view, here are the main benefits for using Lean instead of the currently available alternatives: This is where the Mathlib community is. This is, of course, not a very satisfying argument, and I'll return to it later. I strongly believe that Dependent Type Theory is key to the user experience in Lean. Note that this is not purely a foundational question: of course all of the things I ever formalized would fit into ZFC (+ universes), but the rigidity of type theory is what makes Lean helpful when I write a proof, while dependent typing gives us all the expressive power we could ever wish for. To me, this also rules out Isabelle/HOL. For a better informed opinion, here's a quote from Sébastien Gouëzel's website However, I have been stuck somewhat by the limitations of the underlying logic in Isabelle (lack of dependent types, making it hard for instance to define the p-adic numbers as this should be a type depending on an integer parameter p, and essentially impossible to define the Gromov-Hausdorff distance between compact metric spaces without redefining everything on metric spaces from scratch, and avoiding typeclasses) I am not that scared by bugs in the kernel of Lean (though I am concerned about misunderstood parts of the type theory, see below), because I'm not scared about huge parts of the mathematical literature being wrong. Instead, I view the proof checking abilities of Lean as a safety net that allows proof-writing to be a more "experimental" process: you can refactor a proof dozens of times, try to minimize hypotheses, tweak statements and definitions all over the libraries, and Lean will tell you if and where things break. As a consequence, I wouldn't switch to Metamath "because it is safer", as I don't think the safety gain is worth the usability cost. Finally, I care about human-readability of any formalization. Mathlib (and Lean) are obviously quite far from perfect here, and I wouldn't claim that anyone can read any part of Mathlib (note that AI formalization are a lot worse in this regard). This, along with minor UX issues, justifies my preference for Mathlib over Mathcomp: while I recognize that SSReflect has some selling points, I think they are far outweighed by the cryptic nature of the resulting code. Now that this is out of the way, let me give some real concerns I have about the development and apparent monopoly of Lean moving forward. First and mainly, I am extremely unhappy with the FRO's position on "vibe-coding" and "vibe-proving". I believe the people at the FRO are serious enough that Lean won't become pure slop, but the Lean-slop association is becoming very strong in a lot of people's mind. I am concerned about the FRO trying to establish Lean as the de-facto standard for everything proof-assistant related. I think the recent disastrous quotes from Kevin Hartnett's book are a perfect example of this, and it is embarrassing that the FRO is pushing this book so hard. I am worried about the FRO's relation to the community of researchers in type theory. The last soundness bug has been interesting on this matter because it made me realize that Lean's treatment of so-called "nested inductive types" is kind of a hack. Even before we care about soundness, we should care about having a specification for our foundations, and my understanding is that the FRO has not been very collaborative here. More generally, I am concerned about the development model behind Lean. This is probably my European bias, but I would be much happier if Lean was developed as a research project rather than as a startup. So, right now, for my needs, yes I am stuck with Lean. If I had to switch to another language, that would probably be Rocq, whose development model is very aligned with my values. My (very personal) opinion is that the Mathlib community should invest some energy into making sure that Mathlib survives the Lean hype, which would start by investigating whether Lean's great metaprogramming infrastructure can be conveniently ported to Rocq (as we've learned from the Lean 3 -> Lean 4 port, this is a big feasability prerequisite). But I think porting Mathlib to a non-DTT proof assistant would be not only essentially impossible, but also a significant regression.

Timothy Chow (1): Thanks for the thoughtful response. Let me directly answer your question, "What do you want to do with your proof assistant?" My main question isn't what I personally, as an individual, want to do when I sit down at a terminal and fire up a proof assistant. I'm more concerned about community-wide issues. Let's take one specific prominent issue, just to be concrete: We seem to be entering a world in which people want AI-generated proofs to be confirmed with a proof assistant. Maybe journals will start to announce standards for such verification. Will Lean be the only acceptable standard?

Jason Rute — Score: 6

Here is a point relying on AI progress. We have already seen AI Lean projects getting within an order of magnitude of Mathlib in lines of code. (Mathlib currently has something like 2.5 million lines of code. Here is an AI project with 1.2 million lines of Lean code.) In the near future, it might not be hard to automatically translate math from one formal system to another fairly idiomatically via AI. One could imagine keeping up-to-date libraries of foundational mathematics in Metamath/set.mm (set theory), HOL[4 or -light] (higher-order logic), and Lean (DTT). The first two have very good correctness guarantees and are based on better understood foundations. Metamath is extremely clean, having no automation or complicated type checking. Certainly for important proofs (like RH) it might be worth trying to convert the proof from one system to another, either symbolically or with AI. For the symbolic automatic conversion approach, one interesting mention is that Eliot Glazer claims to have worked out the exact set theory which matches Lean on arithmetic statements, namely ZFC+PFIRS (also see here), and one could build a version of Metamath around ZFC+PFIRS and an automatic conversion tool from Lean to Metamath/ZFC+PFIRS. But symbolic automatic conversion of any kind would have ugly code, so it isn't always the best approach. (There are also other automatic conversion projects like Dedukti and MM0, but I don't know how far they have gotten.)

Elliot Glazer (3): Clarification: the more familiar theory ZFC+$\{n \text{ inaccessibles}: n<\omega\}$ matches idealized Lean on arithmetic. PFIRS has the stronger property that PFIRS proves an arbitrary sentence iff for some $n,$ Lean proves that sentence holds in at least one of the first $n$ universes.

Jason Rute (0): @ElliotGlazer Sorry, I messed that up even after James Hanson corrected me in my other question (proofassistants.stackexchange.com/a/6543/122). But it is correct to say PFIRS is the most equivalent set theory to Lean, right? In that there should be some automatic translation going both ways? Is that correct?

Elliot Glazer (0): Yes such an automatic translation should be possible to program. Once lean4lean is complete I think this will be a natural and feasible followup.

Stanley Yao Xiao — Score: -3

Having no technical knowledge behind theorem provers/proof assistants, and only dabbled with Lean, let me approach this from the angle of economic history. The truth is, for almost all new inventions, the first company to come up with the idea or to deploy it at scale is usually not the one that survives in the long run. For example, many of the first car manufacturers are no longer around, and of the ones that are still around, fewer still are dominant. Some of the most popular brands like Toyota came much later. Even Ford is not among the first car manufacturers. Fast forwarding to electric vehicles, Tesla was undoubtedly the frontrunner, but it is now losing market share rapidly to Chinese brands. The same story plays out over and over again in many industries. The Dot Com bubble famously crushed many early entrants, but there are long term survivors, few of which you would've bet on in 1999 say. As a particular example, Google was not the first search engine. Uber was not the first ride-share company. The point is, this monopoly may not last long, if innovation persists and better products are developed. Given how hard Lean is apparently to use (at least to me), it's not hard to imagine that a much more user-friendly (and hence useful) version, better tailored to the community it serves, will come into existence at some point. The issue is that the mathematical community is small and somewhat economically irrelevant. Leant is free to use as far as I know, and that sets the economic incentive at the bottom. Why would anyone bother to innovate and create a better product if they are going to make no money doing it? That said, the process of 'monetizing' mathematics is accelerating, whether we like it or not. Mathematics is inevitably behind the key innovations that will drive progress in our world in our foreseeable future, and thus technologies that affect mathematics will have an economic incentive. It is not too hard to imagine that there will be real interest among major tech players to work on a proof assistant/theorem prover, because they see it as a valuable investment that will one day improve their bottomline. At that point, it is hard to imagine that the clunky Lean as it exists today will stand a chance.

András Kovács (27): This answer is pretty much all wrong. Lean is very far from being the first proof assistant, it arrived relatively late and a key reason that it got popular was that it had a stronger focus on user experience, ergonomics and ease of setup than other systems. "Clunky system with first mover advantage" is roughly the opposite of what happened.

Stanley Yao Xiao (1): @AndrásKovács If Lean is in fact not close to being the first, I would still say that it is far from being successful at providing a smooth user experience or a gentle-enough learning curve. I still can't imagine it being a part of standard graduate training for mathematics students in the same way that LaTeX is, for example. The room for improvement is still massive

Timothy Chow (2): @StanleyYaoXiao I agree with you regarding incentives and room for improvement. I highly recommend the book Mechanizing Proof by Donald MacKenzie. It is an excellent account of the early history of proof assistants, and it also tells the story of how the U.S. government became very interested in formal verification for a period of time during the late 20th century, only to become disillusioned once unforeseen difficulties were encoutered.

Yemon Choi (2): I just wanted to second @AndrásKovács's comment. I know very little about math(s) formalization but I do take an interest in what people are doing, and the fact that well-educated young(er) mathematicians can even think Lean is a first-mover is mildly depressing to me. Did Thomas Hales hector us in vain? ;-)

Emil Jeřábek (6): I don’t think the situation is comparable to the (fairly free) car market, as the “vendor lock-in” is much higher here. You can’t just replace your old Ford proof assistant for a Toyota proof assistant even if it’s much superior, unless you are willing to lose all the proofs you’ve already formalized and redo them from scratch, not to mention the huge library of theorems that other people have formalized in Ford.

Are we stuck with Lean?