Are We Stuck with Lean?
摘要
MathOverflow 上一位数学家提问：数学社区是否已被 Lean 证明助手锁定，以及是否有机构会支持 Metamath 等替代品。回答者包括 mathlib 维护者、依赖类型批评者、AI 形式化研究者等，观点分歧：有人认为工具是社会现象、垄断不会持久，有人指出 AI 生成证明代码已接近 mathlib 规模，未来可能自动翻译形式系统，也有人批评依赖类型的根本缺陷。整体是围绕证明助手生态、AI 验证、形式化数学未来的多元讨论。
荐读理由
正文提供了两个可迁移的洞见：一是 AI 生成证明代码已达 mathlib 近半规模，说明 AI 在形式化数学上的能力正在快速逼近人工水平；二是自动翻译形式系统的设想（如 Lean 到 ZFC+PFIRS）可能打破单一证明助手的垄断，这直接影响你对 AI 在代码验证、形式化工程领域机会的判断。
原文
33
$\begingroup$
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. :-)
asked 12 hours ago
94.2k3434 gold badges425425 silver badges682682 bronze badges
$\endgroup$
30
5 Answers 5
28
$\begingroup$
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.
answered 11 hours ago
12.3k44 gold badges4848 silver badges8787 bronze badges
$\endgroup$
$\begingroup$
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!).
2,72466 gold badges3939 silver badges4343 bronze badges
answered 11 hours ago
3,89044 gold badges4040 silver badges5454 bronze badges
$\endgroup$
$\begingroup$
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.)
answered 6 hours ago
6,59122 gold badges3535 silver badges5757 bronze badges
$\endgroup$
$\begingroup$
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]
answered 6 hours ago
76188 silver badges1212 bronze badges
$\endgroup$
0
$\begingroup$
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.
answered 12 hours ago
33.1k88 gold badges7474 silver badges187187 bronze badges
$\endgroup$
Start asking to get answers
Find the answer to your question by asking.
Explore related questions
See similar questions with these tags.
这条对你有帮助吗？