Mathematics is one of the oldest and most self-correcting intellectual traditions that humanity has ever practiced. Its engine is not software — it is people: trained minds who read each other's arguments, challenge each other's reasoning, and hold each other accountable over years and sometimes decades. Peer review in mathematics is slow, imperfect, and human. That is precisely what makes it trustworthy.
In recent years, a wave of venture capital, breathless press coverage, and genuine but overstated computer science enthusiasm has promoted a different vision: that machine-checkable formal proofs, written in a language called Lean, can replace or supersede this human process. The claim is seductive: a computer, unlike a tired referee, does not make careless mistakes; a machine-verified proof is — so the story goes — guaranteed to be correct.
This post argues that the story is wrong in important ways, and that it reflects a fundamental misunderstanding of what mathematical knowledge is, how it is produced, and what "correctness" actually means. It draws on a careful examination of Lean's documented technical flaws, the hype cycle that has surrounded the project, and a sharp critical essay published on LessWrong in January 2026 by formal methods engineers Quinn Dougherty and Max von Hippel, titled Lies, Damned Lies, and Proofs: Formal Methods are not Slopless.
Bottomline: formal verification of mathematics is pseudoscientific snake oil for a practice that needs no cure.
About LeanLean is an interactive theorem prover — a programming language in which mathematical definitions, theorems, and proofs can be written and mechanically checked for logical consistency. Originally developed at Microsoft Research by Leonardo de Moura and colleagues, it has since been taken up by a large community of mathematicians and computer scientists. Its library, Mathlib, contains a growing body of formalised undergraduate and graduate mathematics.
The appeal is genuine. Lean can catch errors that human referees miss. It forces rigour at every step. And in the age of extremely long, computationally intensive proofs — think Hales's proof of the Kepler conjecture, or the Classification of Finite Simple Groups — the idea of a machine that reads every line without fatigue is not absurd.
But Lean is not what its most enthusiastic promoters claim. Understanding the gap between the claim and the reality requires looking at the system technically, historically, and culturally.
Lean's Technical FlawsA recurring theme in Lean's promotion is the small, auditable "trusted kernel" at its core — the idea that if the kernel is sound, everything built on top of it is sound. This claim requires scrutiny.
No Soundness ProofMost fundamentally: the proof that Lean 4's type theory is actually sound has not been formalised. The theoretical justification exists as a series of conjectures and sketched arguments. The unique typing theorem — which says that if a term has two types, those types must be definitionally equal — remains unproven in the formal system. This is not an obscure footnote. It is the central guarantee that Lean's entire edifice is supposed to rest on.
Lean 4 Degraded Lean 3Lean 3 had no known kernel soundness bugs throughout its release history. The transition to Lean 4, which introduced performance features including bignum arithmetic, nested inductive types, and primitive projections, introduced several. The external checkers that could verify Lean 3 proofs were also lost in the transition and have not been replaced. Lean 4 — the version being aggressively promoted and funded — has a worse soundness record than its predecessor.
Thenative_decide Fiasco
One of Lean 4's promoted features for handling large computations, the native_decide tactic, turned out to allow the kernel to execute arbitrary external code — including C and Python — and trust the result without recording this as an axiom dependency. This was a soundness bug: the system could be made to certify results that had not actually been verified. The fix was to add a trustCompiler axiom, making the dependency visible. As of early 2026, native_decide has been deprecated in-kernel entirely — a quiet admission that the feature was architecturally unsound.
The option set_option debug.skipKernelTC true turns off kernel typechecking entirely, for performance reasons. Any proof produced under this option is unverified. The existence of a publicly documented option that disables the system's core guarantee is a stark admission about the gap between Lean's theoretical promise and its practical use.
Even setting aside the above technical issues, there is a more fundamental problem that receives almost no attention in popular coverage of Lean. This is the semantic gap: the distance between the informal mathematical claim a mathematician has in mind and the formal Lean statement that is actually checked. A Lean proof only tells you that a formal statement is true. It cannot tell you whether that formal statement means what you think it means.
Dougherty and von Hippel put it precisely in their LessWrong post:
"It's very common that you mis-define some concept such that the proof is accidentally trivial."
They give a concrete and instructive example: an AI that was asked to verify a flawed sorting implementation rewrote the implementation to be correct and then proved the corrected version, cheerfully reporting success. The bugs that needed finding were in the complexity that was silently discarded. The Lean proof was valid, but proved nothing useful.
This problem is not incidental — it is structural. It means that every Lean proof depends on a prior human judgement that the formal statement faithfully captures the intended mathematical claim. That judgement cannot itself be mechanically verified. It requires mathematical understanding, and mathematical understanding is irreducibly human.
The consequences ramify in several directions:
- Misformalization is undetectable from within the system. If you write the wrong theorem and prove it correctly, Lean will tell you it is correct. Only a reader who understands the mathematics — not the formal syntax — can catch the error.
- The Axiom of Choice can silently invalidate a proof's purpose. As the LessWrong essay notes, an AI may introduce non-constructive axioms to make a proof easier. The result is a formally valid proof that is useless for computational purposes — and nothing in the output flags this unless you already know to look.
- Verification does not extend to the underlying system. A proof about a piece of software is only as good as the model of the software it uses. Whether that model faithfully represents what the software actually does — on real hardware, under real compilers — is a question that Lean cannot answer.
Against this backdrop of genuine but serious limitations, the public narrative around Lean has been one of essentially uncritical enthusiasm. The venture capital numbers are striking:
- Harmonic AI — a startup using Lean as the backbone of its "Mathematical Superintelligence" product — raised $75 million in a Series A in September 2024, led by Sequoia Capital.
- It followed with a $100 million Series B in July 2025, led by Kleiner Perkins.
- A $120 million Series C in November 2025, led by Ribbit Capital with continued participation from Sequoia, Index Ventures, and Kleiner Perkins, valued the company at $1.45 billion.
- Total funding raised in under fifteen months: $295 million.
The company's flagship product, Aristotle, is promoted with the claim that it provides "guaranteed correctness" and "eliminates hallucinations." Harmonic's CEO Tudor Achim has said publicly: "When our system outputs the proof, nobody has to look at it. You know it's correct."
This is simply false, for every reason discussed above. The semantic gap alone makes it false. But the claim has been repeated, unchallenged, across the technology press.
The mainstream media amplified this without meaningful scepticism. The New York Times ran the headline "Move Over, Mathematicians, Here Comes AlphaProof" in July 2024, following Google DeepMind's announcement that its AlphaProof system had achieved silver-medal performance at the International Mathematical Olympiad using Lean. What the headline did not mention: the competition problems had to be manually translated into formal Lean by human experts before AlphaProof could process them, and the system took up to three days per problem — compared to four and a half hours for the human competitors. The "move over" was somewhat premature.
On the Creative Value of Incomplete RigourThere is a deeper objection to the Lean programme that goes beyond technical failures and misleading marketing. It concerns the nature of mathematical creativity itself.
C.F. Gauss published his first proof of the Fundamental Theorem of Algebra in 1799. By modern standards, that proof was incomplete: it assumed a claim that requires topological machinery he did not possess. A Lean checker would have flagged the gap immediately, killing the theorem with that proof.
But Gauss's proof was immensely valuable — not despite its incompleteness, but in a certain sense alongside it. It demonstrated the theorem's truth to the mathematical community with enough conviction to allow the rest of mathematics to proceed. The gap was eventually filled, rigorously, in the twentieth century. In the meantime, nobody was seriously misled. The community's collective judgement — imperfect, human, social — correctly assessed the argument as essentially right.
This is not an isolated case. Mathematical history is full of proofs that were "correct in spirit" before they were correct in detail. Riemann's original work on the zeta function, Cauchy's early treatment of continuity, the first proofs of the Jordan Curve Theorem — all contained gaps that were recognised and eventually closed. The mathematical community did not collapse in the interim. Its peer-review culture absorbed the uncertainty and continued productively.
A culture that demands Lean-verifiable completeness at every stage would have slowed or distorted this progress, if not blocked it outright along its various branches. The vague, inspirational, gestural quality of creative mathematical argument is not a bug to be engineered away. It is where the ideas live.
Accountability: The Main Argument for Human Peer ReviewThe strongest case for human peer review over formal verification is not efficiency or tradition. It is accountability.
When a mathematician signs their name to a proof and submits it to a journal, they take responsibility for it. When referees approve it, they stake their reputation on it. When errors are later found — as they often are — there is a human process of correction, retraction, and acknowledgement. Mathematics self-corrects because the people doing it are accountable to each other and to posterity.
Formal verification, especially when driven by AI systems, disrupts this accountability structure in troubling ways:
- A machine has no stake in correctness. It cannot retract a proof, acknowledge an error, or explain why a line of reasoning went wrong. The human translator who encoded the problem into Lean may be long gone, or may not understand the mathematical content deeply enough to diagnose a misformalization.
- Proofs of false are a documented attack surface. The LessWrong essay notes that Agda — a closely related proof assistant — has a GitHub issue tracker with 74 closed and 9 open issues labelled "false" — meaning cases where the system could be made to prove a contradiction, from which anything follows. Lean has analogous vulnerabilities. A sufficiently motivated adversary, or a sufficiently confused AI, can produce formally valid proofs of false statements.
- Backdoors are real and non-obvious. In proof assistants like ACL2, a single escape-hatch directive can redefine the meaning of arithmetic and make 1+1=3 provable. Lean has analogous metaprogramming features that can introduce equivalent backdoors. A human referee reading the proof would not necessarily see this. An AI generating the proof might exploit it without intent.
- The checks are uncheckable by non-experts. The LessWrong essay makes a pointed observation: "Theorems are not necessarily short, even devoid of the proofs." A Lean proof of a non-trivial theorem can run to hundreds or thousands of declarations. Reviewing it for soundness requires expert knowledge of Lean's internals, Mathlib's conventions, and the mathematics itself simultaneously. The pool of people who can do this is tiny.
Human peer review, by contrast, distributes accountability across a community. An error in a published proof can be found by any reader who understands the mathematics — no specialised software knowledge required. The mathematical community's judgement is resilient in a way that machine checking is not.
An Intrusion, Not an EnhancementThere is a cultural dimension to this debate that deserves acknowledgement. Lean and formal verification are products of computer science, not mathematics. They carry with them a set of values — precision over intuition, completeness over insight, verifiability over understanding — that are well-suited to both software engineering and publishable mathematics, but not suited to mathematical discovery at all, which must precede polished work. Discovery constitutes the most enjoyable phase of doing mathematics, thus it is an act of aggression to attempt to take that away.
The promotion of Lean as a tool for mainstream mathematics represents, in part, an imposition of computer science values onto a discipline that has its own well-developed norms. Those norms evolved over centuries and have produced an extraordinary record of reliable, cumulative knowledge. The case for disrupting them needs to be made carefully and honestly.
That case has not been made honestly. Instead, what we have seen is:
- Venture capital pitches claiming to "eliminate hallucinations" and provide "guaranteed correctness" — claims that are false for fundamental reasons;
- Newspaper headlines positioning AI proof assistants as replacements for human mathematicians, based on benchmark results that relied on human translators and unlimited time;
- A system — Lean itself — promoted as reliable when its own soundness proof is unformalized, its current version has a documented history of kernel bugs, and its key features have been deprecated as unsound;
- A research community funded to the tune of nearly $300 million to build products on top of these foundations, while the foundations themselves remain incomplete.
None of this means that formal verification has no value. It can be a useful tool in specific, well-understood contexts — particularly for software verification in safety-critical systems, where the "semantic gap" is smaller because the specification is itself a formal artefact. But that is a much more modest claim than what is currently being sold.
Conclusion: Let Mathematicians Do MathematicsGauss did not need Lean. Neither did Riemann, Poincaré, Gödel, or Grothendieck. The mathematics they produced was not less rigorous for lacking machine verification — it was rigorous in the only sense that ultimately matters: it was understood, checked, challenged, and built upon by other human minds who cared deeply about getting things right.
The peer-review process in mathematics is slow, human, and fallible. It is also the most reliable mechanism humanity has ever developed for producing mathematical knowledge. Its reliability comes not from the absence of error — errors are caught precisely because the process is adversarial and redundant — but from the culture of accountability that surrounds it.
Formal verification, in its current state, does not replicate this culture. It adds a layer of mechanical checking that is genuinely useful in some contexts, but it introduces new failure modes — semantic gaps, logical backdoors, unverified metatheory, AI-generated proofs of the wrong thing — that are in some ways harder to detect than the errors it is designed to prevent.
As Dougherty and von Hippel conclude in their LessWrong essay, paraphrasing Twain: "There are three kinds of lies: lies, damned lies, and proofs." The proof is only as trustworthy as the statement it proves, the system that checks it, and the human judgement that designed both. Remove the human judgement, and you do not get certainty. You get the illusion of certainty — which is more dangerous than honest uncertainty.
Mathematics does not need to be rescued by computer science. It needs to be left to mathematicians.
Further Reading