对Lean4形式化证明的批判性审视

Lots of the discussion around Lean certificates and trust centers around general philosophical ideas of how much humans should trust formal certificates. It's important to remember, though, that Lean4 is not an ideal formal certificate machine: Lean4 is a software in its infancy and has issues. There are reasonable reasons to specifically not trust Lean4.If we're going to be putting our society's trust in Lean4, I think that it's good to have an open critical discussion of how warranted that trust is.Epistemic status: Most of this work is a factual description about aspects of Lean4 and set theory. I am 85% sure that at most two of these factual descriptions are incorrect. I am 90% sure that, in the current version of Lean4 on Github, there exists a proof of the statement "True=False" that would be accepted in such a way that the Lean community would call it a bug in need of patching (either by messing with the elaborator, compiler, kernel, or some other part of the Lean). I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs, and that the human work we do as a community thinking about and fixing Lean4 in the next 24 months would fall under Less Wrong's classification of a pivotal act.The current status of thingsHere's a quote from a last April be Leo de Moura, the creator of Lean.Here's another post by Leo de Moura, three months later:Following this incident, the Lean FRO found seven more bugs in the kernel. The new opinion of Leo de Moura: "[False statements being accepted by Lean] is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels".What was the Lean community's reaction to "soundness bug #14576"? There's a nice thread about it on a Lean developer's forum here.Uh oh! Not only do we expect bugs, but there are possibilities of "sea monsters". This article is a bit about the bugs, a bit about the sea monsters, and a bit about the unsafe ways that Lean4 is currently being used (e.g. the un-sandboxed comparator used in Anthropic's formalization of Fermat's Last Theorem) .What does it mean for Lean4 to be consistent?Lean4 lets you write mathematical statements and proofs using the bare low-level primitive notions of mathematics, and checks that the proofs are valid using the fundamental axioms. Which axioms? The most standard mathematical axioms are the "Zermelo-Fraenkel plus Choice" axioms (ZFC). These axioms have been vetted by armies of nerds and we're really quite certain that they are consistent. Lean4 is not based on ZFC. It is based on a special home-brew version of dependent type theory, which was designed by picking and choosing features of various modern type theories, with the governing design principle that it should be fast at compile time.How do we know that Lean4's type theory is consistent? Ideally we would construct some totally convincing proof that if ZFC (or some standard strengthening of of it via large cardinal axioms) is consistent, then Lean4 is consistent. However, we currently don't know how to do this.As of writing, there is no publicly available proof that Lean4 is consistent with respect to ZFC + any large cardinal axiom.When I originally learned that Lean4 had no known consistency proof, I thought this was some sort of bug or technicality. Surely we understand why Lean4 is supposed to be consistent, we just haven't bothered writing out the details? My current read of the situation is that this is not the case. Lean4 is not known to consistent, we don't know why it should be consistent, and there are real obstructions to all known proof strategies for showing that Lean4 is consistent.Smart people make fundamentally inconsistent type theories all the timeLean4 is a "dependent type theory". Dependent type theory as a foundation for mathematics was pioneered in 1971 by Martin-Löf. A year after Martin-Löf came out with his type theory, Girard found a contradiction in Martin-Löf's theory. In his revised paper, Martin-Löf concluded that one of the axioms “had to be abandoned” and describes the necessary change as “so drastic” that the theory lost substantial expressive strength. Oops! Constructing good dependent type theories is hard.Outside the world of dependent type theory there are other famous examples of mathematicians trying to come up with new foundations of mathematics and making deep, subtle, fundamental mistakes: Church's 1932 proposed foundations for mathematics using lambda calculus (which was shown to be inconsistent by Kleene and Rosser), and Quine's 1940 proposed reworking of ZFC (which was shown to be inconsistent by Rosser).The status of Lean4's consistency proofComing up with consistent foundations for math is tricky business. The ingredients that make Lean4 fast at compile time are the same ingredients that give it access to an unusually strong amount of recursion. For instance, a common proof strategy for showing that dependent type theories are consistent with respect to ZFC + large cardinals is to use the so called "normalization" property. It was proved in 2019 by Abel and Coquand that this normalization property fails for type theories like Lean's, which in some precise sense means that Lean4's type theory is wild/poorly behaved.There was a proof of Lean3's consistency proposed in 2019 by Mario Carneiro. This proof works by embedding the primitive notions of Lean3 into the primitive notions of set theory (sets, functions between them), and then showing that the axioms of Lean3 correspond to true statements about sets. Proving that type theories are consistent with respect to ZFC + large cardinals via embedding into set theory is standard business. Unfortunately it came out in 2024 that there was a flaw in his proof strategy (oops!) and that the correct proof would require a new approach. Even if the Lean3 embedding gets fixed, Lean4 adds new features which require non-trivial extensions of that embedding.I recently asked my GPT-6 Astra to find an embedding of Lean4 into set theory. It spent ~25h and several thousand dollars on the task, and it did not succeed. It kept trying new embeddings and tricks, but every time it found counterexamples using the strong recursive power of Lean4. So it seems to me like finding this set theory embedding is a genuinely non-trivial task, and we don't have a high-level picture of why Lean4 should be consistent.Untamed recursion is bug-proneOne of the main things which makes Lean4 logically complex are its "nested inductive types", a sort of declaration where you can define a type in terms of a higher-order property of its own type. Nested inductive types are a new research area, but our understanding is still in its infancy (we've had some good progress in 2026, here and here). Preliminary evidence suggests they might be pretty wild. Here's a quote from the former of those two papers:"Considering the importance of nested inductive types, one would expect Rocq and Lean to offer good support for them, yet neither one does. They both fail to generate usable elimination principles, and surprisingly accept a different set of nested inductive types, neither of which is satisfactory...[technical paragraph about a problem with Lean's implementation of nested inductive types] ... this workaround highlights the need for a more systematic treatment of the problem—one that avoids such leakage of the internal encoding. More problematic, since a straightforward mutual encoding becomes impractical in more complex scenarios, Lean ultimately rejects some nested definitions that are theoretically valid—and often crucial for advanced specifications.These implementation shortcomings likely stem from an incomplete foundational understanding of nested inductive types."The conclusion from the literature, in my view, is that even if Lean4's type theory is consistent at a high level, the nature of nested inductive types makes Lean4's recursion wild. That behavior could be so wild that it is fun