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 .
Here'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 ) .
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.
Lean4 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 ).