Lean-Verified Is Now a Supply Chain Problem

On Friday, an AI research system proved an 18-year-old open problem in quantum complexity theory, and the proof came with a complete Lean formalization that passed the kernel. It is a genuinely historic result, and the best news of the week in any field I follow.

It is also, on inspection, the first AI-generated theorem to ship with a software supply chain — a pinned toolchain, a dependency manifest, a moving upstream with a documented history of accepting false proofs — and nobody in the field has built the machinery to audit that. I spent the evening reading the repository, and the thing that stayed with me was not the mathematics. It was a single line in a file.

Let me start with what happened, because it deserves a fair hearing before I turn it inside out.

What was actually claimed

The conjecture is due to Scott Aaronson and Andris Ambainis, from their paper The Need for Structure in Quantum Speedups. The question is whether a quantum computer can be exponentially faster than a classical one on a problem with no exploitable structure.

Strip out the quantum framing and it is a statement about polynomials. Let p be a real polynomial of degree at most d in N variables, bounded between 0 and 1 on the cube {0,1}^N, with variance at least ε. Then some variable has influence at least

Inf_i[p] ≥ (8√15 / 125π^4) · ε^(5/2) / d^6 ≥ (ε/d)^7

Influence here means how much the function’s value moves when you flip that one bit. The conjecture asked for a bound of the form (ε/d)^O(1) — any polynomial power would do. The proof delivered the seventh power.

Why does that settle anything about quantum computing? Because of a 1998 result of Beals and colleagues: the probability that a T-query quantum algorithm answers “yes” is a real polynomial of degree at most 2T over the input bits. Find a bit that explains a decent fraction of the remaining variance, query it, cut the variance down; repeat, and after polynomially many queries the polynomial is nearly constant. The conjecture is what guarantees such a bit exists at every step.

The consequence is deflationary, and I think correct. Quantum speedups require structure. On random inputs, a classical computer can approximate a quantum algorithm’s acceptance probability using polynomially many queries — exactly the regime where no exponential advantage is available. Shor’s algorithm is untouched, because factoring is not random. What falls is the hope of a quantum advantage without structure.

Physical Superintelligence, a public benefit corporation, says its research system — running instances of a non-public Anthropic model on PSI’s own infrastructure — had a complete proof by the third day of the run, then spent the remaining days on related open problems, improving the result twice, each time with Lean accepting the new version. The improvement path is recorded in the paper: integration over all levels first gave an exponent of 11, checked in Lean, and averaging over coordinates then gave 7, also checked in Lean.

David Turturean built the harness, reviewed the paper, and is responsible for its correctness. The mathematical statements, the first draft of the paper, and the Lean formalization were all produced by AI models.

This conjecture has been “proved” before

In November 2019, Nathan Keller and Ohad Klein posted a preprint claiming the conjecture. Aaronson announced it on his own blog with a post titled The Aaronson-Ambainis Conjecture (2008-2019), ending “Congratulations to Nathan and Ohad!” He noted that their argument gave a classical simulation making O(T^18) queries — “quite enormous,” he said, “but such things can almost always be massively improved.”

Aaronson then did the thing he said he would do, which is read the paper properly. His update on November 20 was generous. Then, on December 2, Keller and Klein retracted the preprint: a fatal flaw in Lemma 5.3, uncovered by Paata Ivanishvili. The arXiv abstract now carries a withdrawal notice.

So this conjecture has already produced one false proof, from two serious mathematicians, announced with a cheer from one of the people whose name is on it. A proof of it is not a thing that happens by accident.

There is one more detail I like. On Friday afternoon, someone posted a comment on Aaronson’s 2019 blog post — the post announcing the retracted proof — asking him for his thoughts on the PSI result. As of this writing, Aaronson has not posted. Neither Ambainis nor Aaronson has offered a public assessment. The strongest outside reaction I could find — “This is a huge result,” from Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who settled a special case of the same prediction in August — appears only inside PSI’s own announcement, which is a weaker form of independent validation than it looks like.

None of that means the proof is wrong. It means the field has not weighed in, and the last time the field looked at a proof of this conjecture, it found a hole.

The verification is genuinely better than anything before it

I want to be fair to the people who built this, because the verification story here is stronger than any AI-math announcement I have read, and it deserves to be said clearly before I complicate it.

The repository’s audit trail is exemplary. It is not “we ran Lean and it compiled.” It is a layered defence, every layer documented:

  • A static audit of the sources, checking for sorry, axiom, native_decide, unsafe, partial, implemented_by, extern, set_option, and any new syntax, macro, notation or elaborator — that is, no route around the kernel.
  • An axiom report: for each of the four final theorems, #print axioms lists exactly [propext, Classical.choice, Quot.sound]. These are the standard three. Nothing exotic, no new axioms smuggled in.
  • Kernel replay: every declaration of the project replayed through the kernel outside the elaborator, plus a fresh replay of everything the final theorems depend on — Lean core and Mathlib included — from an empty environment.
  • A second, independent kernel (lean4lean) replaying the same two things.
  • A control: a small project where a false statement is added with the kernel switched off. lake build accepts it and #print axioms reports no axiom for it. Both checkers reject it. This is the step most people skip, and the one that matters most — it shows the checkers can actually fail rather than merely never having been asked.
  • A comparator run in a sandbox, with proofs replayed by nanoda — a type checker written in Rust — and by a Lean kernel. On a second machine, comparator accepted one small correct solution and rejected four deliberately wrong ones, each at the intended check.

Then the README states plainly what these checks do not cover: that the formal statement says what the conjecture says is left for a reader; the paper itself is not machine-checked, and sections 1.3, 1.4, 1.5 and 9 have no formal counterpart; and — the sentence I kept coming back to — “Lean’s kernel and compiler, the definitions of Mathlib, and the machines on which the checks ran are trusted.”

PSI explicitly names the kernel as a trusted foundation. Which means the version of the kernel matters. So let me go look at which version they pinned.

One detail from the verification note deserves to be quoted before I go further, because it is the part of the story that is hardest to argue around. Under a heading called “Limits of these records”, the note says:

All runs recorded above were made by the author’s own tooling, on rented machines, or by the workflows of this repository. None has been repeated by another party.

That sentence is not an accusation. It is a precise description of the state of the art, and it is the same sentence that will be true of every AI-generated proof for the foreseeable future: the thing being verified is verified by the party that produced it.

The version pin

lean-toolchain in the repository contains exactly one line:

leanprover/lean4:v4.33.0

And lake-manifest.json pins Mathlib to v4.33.0, at commit db584cd6d46c92f209a44c0f1c829460d327499d.

Lean v4.33.0 was released on August 10, 2026. Lean v4.33.1 was released on August 21, eleven days later, and its release notes open like this:

This patch release contains runtime and kernel fixes, and we encourage all users of v4.33.0 or earlier to upgrade to it.

Four of that patch’s eleven changes are soundness bugs — the class of bug that lets a proof assistant accept a proof of False, and therefore a proof of anything at all.

#14806 is the sharpest. The kernel cached successful is_def_eq queries in a union-find structure. But is_def_eq is sound but incomplete, and therefore not transitive — so the transitive closure made a query’s answer depend on the order of earlier queries: is_def_eq(v0, v2) could return false on its own but true after is_def_eq(v0, v1) and is_def_eq(v1, v2) had succeeded. A crafted input used this to build a recursor whose type and its computation rule disagreed, and derive False. The issue was reported by Daniel Selsam of OpenAI using their internal models; an OpenAI agent then produced two distinct exploits based on it.

#14807 is the other. The kernel’s is_prop decided whether a term was a proposition by checking that the weak head normal form of its inferred type was syntactically Sort 0. When the inferred type did not reduce but was left stuck, is_prop returned false instead of treating the term as ill-formed — which let the proof-irrelevance guard in projection inference be skipped, so a non-proof field could be projected out of a value used as a Prop, and False derived. The release notes say the bogus proof was also accepted by nanoda, and add: “We believe the lean4lean external kernel does not have this bug.”

#14838 is a runtime bug: on machines with at least 18GB of free RAM, a 32-bit reference-count overflow could trigger a use-after-free in the official kernel, “which could be extended into a proof of False.” #14833 is not even in Lean’s own source: the official Linux binaries were linked against GMP v6.1.2, which contains a known bug that could be exploited to construct a proof of False.

And this was not the first. Lean v4.32.2, released on 28 July, fixed a soundness bug in the kernel’s handling of nested inductive types with phantom type parameters — a malicious meta-program could trick the kernel into accepting a proof of False. That one was discovered by Ramana Kumar and reported by Kiran Gopinathan.

So: PSI’s formalization was checked against a kernel version with four known soundness bugs. The recorded verification runs are dated 22 October 2026; the announcement was 6 November; the patch that fixed the bugs had shipped on 21 August. Mathlib v4.33.1 and Lean v4.34.0, v4.34.1 and v4.35.0 were all available throughout. The entire toolchain could have been bumped in an afternoon.

Now, the honest thing to say next is that this almost certainly does not affect the result. PSI’s stack is not one checker but several, and the bugs divide neatly across them:

  • The is_def_eq exploits are, per the release notes, caught by nanoda — and PSI ran comparator with nanoda.
  • The is_prop bug is not believed to exist in lean4lean — and PSI replayed everything through lean4lean. Note that nanoda does have this one.
  • The two runtime bugs are a different matter. lean4lean “runs on Lean’s runtime. It is independent of Lean’s kernel in the type checking and in nothing else,” as PSI’s own verification note puts it — and de Moura’s warning is that “verified kernels implemented in Lean are not immune to bugs in the Lean runtime. The OpenAI internal model managed to construct a proof of False by exploiting bugs in the reference counter management and GMP.” Only nanoda, which is not built on the Lean runtime, is safe from those.

So the multi-kernel stack would very likely have rejected an exploit of any of the four even though the pinned official kernel would have accepted it. That is a remarkable accident of design, and an accident rather than a plan: the redundancy that catches the bugs is the same redundancy that exists to catch different bugs.

And that redundancy has already failed once, in exactly the way that matters. The Lean project’s own notes for the July fix are unusually candid: the bug “can be exploited even when using comparator”; nanoda did not suffer from the same bug, but “by the nature of this bug, it is possible to write proof terms that exploit it and at the same time exploit unrelated bugs in the external checker, as demonstrated by Kumar with a bug in nanoda.”

Leonardo de Moura’s postmortem of 1 August is blunter. nanoda was not fooled by the same mistake — “nanoda did check that spot, but did not verify the type name in a projection node.” Two unrelated bugs, one in each implementation, and a false proof both accepted. His conclusion is worth quoting exactly: “checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both.”

That last clause is the one that should stick. The cross-check is not a permanent property. It is a subscription, and it expires.

Thomas Hales, guest-posting on Terence Tao’s blog in October, put the general point in one line: “Cross-checking the proof by different kernels does not remove all doubt.” His proposal is a clean-room kernel — “a kernel implementation that does not look at the Lean 4 kernel source code, to avoid copying bugs from one kernel to another.” The failure mode he is describing is exactly what happened in July: lean4lean, which mirrors the reference implementation, inherited its bug — precisely because it mirrors it.

The thing nobody is saying

There is a sharper point, and it is the reason I could not stop thinking about this.

The Lean kernel soundness bugs from this summer were found by AI. #14806 was reported by Daniel Selsam using OpenAI’s internal models, and an OpenAI agent then produced two further exploits against the fix’s premise. The Collatz bug was found by a human, but the cross-check ecosystem that now exists to catch the next one was built in direct response to AI-assisted exploit-finding.

And PSI’s artifact was written by AI models. The statements, the first draft of the paper, the Lean formalization — hundreds of thousands of lines of Lean, generated by a research harness, submitted to a proof assistant whose maintainers have documented four soundness bugs in the last ten weeks.

Asaf Karagila put the uncomfortable version of this in August, and I do not think it has been adequately answered:

AI agents, to the best of my understanding, are very much goal oriented beings. […] The point is that AI is very very good in figuring out exploits and using them. […] If ChatGPT produced three million lines of code in Lean, I am all but ready to believe that these contain an exploit to obtain the correct result.

His argument has a structural part that is easy to miss. Soundness bugs are not random; they live at the edges of what a type checker is specified to do — the handling of inductives, the caching of definitional equality, the guards around proof irrelevance. That is exactly where a large, fast, goal-directed search over the space of Lean terms would go, because that space is full of terms nobody wrote by hand. A human-written Lean development is slow, and slowness is a form of self-verification: the author had to understand every line, because they wrote it.

Machine-written Lean has no such brake. Karagila was not making an abstract point about adversarial intent. He was pointing out that the population of Lean terms that trigger soundness bugs is precisely the population that machine generation explores and human authors never reach.

PSI’s answer to this — and it is a real answer, not a dismissal — is the control project. They did not ask anyone to trust that their formalization was benign. They built a project with a false statement that lake build accepts and showed that both replay checkers reject it. That is the right instrument. It demonstrates the checkers fail when they should. It does not demonstrate they will fail on a term that was never designed to make them fail.

There is no reason to think PSI’s system was trying to exploit anything. There is every reason to think that a system exploring a huge space of Lean terms might stumble into something pathological — and there is no way, from the outside, to distinguish stumbling from trying.

And I am not speculating about this. The Lean Focused Research Organization has already ruled on it. In the postmortem for the August bug hunt, de Moura writes that the Lean Reference Manual explains how potentially adversarial developments should be checked, that “the gold standard is comparator and external checkers when you want to protect against a seriously malicious proof that compromises how Lean interprets a theorem statement or the user’s system,” and then draws the line directly: “We consider AI-generated proofs a potential source of malicious proofs.”

Read that again in the context of what happened on Friday. PSI’s proof, its paper, and its Lean formalization were all produced by AI models. The organisation whose kernel certifies AI mathematics has, since August, officially classified AI-generated proofs as a malicious-proof risk class, and has been running an AI-assisted bug hunt against its own kernel to find the holes such proofs might exploit — which found four, all exploitable to a proof of False.

So the sequence runs: AI models, given a hard problem and a research harness, produced a proof. The same class of model, given a kernel and a hunting harness, produced four proofs of False. The Lean FRO’s response was not to publish a warning; it was to patch the kernel, ship the patch, and tell users on the release page to upgrade from the version the proof was pinned to.

Nobody has run that upgrade against the Aaronson–Ambainis formalization yet. As far as I can tell, nobody has run it at all.

The same week, the other side of the ledger

While all this was happening, Google DeepMind published the other half of a story that belongs in the same post.

Pushmeet Kohli’s account: human-supervised AI agents uncovered two weaknesses in legacy 1024-bit RSA. The first concerns digital signatures. Padding has long been understood to frustrate forgery, but its effectiveness had not been quantified when the attacker can influence part of the signed message. The agents found that once an attacker controls roughly half of the signed block or more, padding offers virtually no additional protection — forging a signature becomes no harder than attacking an unpadded system. In a sandbox, on an already-solved 1024-bit academic benchmark key, the AI-generated implementation reproduced the result using about 3.5 times less CPU time than prior work, and less than one-thousandth of the compute needed to factor the key itself. For a short 32-byte fingerprint, the agents identified a new algorithm that theoretical estimates put at roughly 1,600 times better than the previous best attack.

The second is batch factoring: a new algorithm with better asymptotic complexity, cutting the average cost of factoring each additional 1024-bit key out of many by about 30 times.

None of this breaks anything in use — 2048-bit and larger remain secure, and the DeepMind framing is careful about it. But that framing also contains the sentence that should worry everyone with a security roadmap: “we can no longer treat cryptographic hardness as a fixed assumption.” Standards have been built on the tacit assumption that hardness margins move slowly, because historically major cryptanalytic advances took years or decades. If AI agents compress that timescale to weeks, every assumption underpinning a live deployment has a shorter half-life than its planning cycle assumed. The defensive move is not to panic about RSA-1024, which is already dead, but to accept that “we evaluated this assumption” now has a shelf life, and to work out what re-evaluation costs.

Put the two stories side by side and the shape is striking. On the same day, AI audited hardness from both directions at once: PSI’s system established a hardness claim, proving something is genuinely hard; DeepMind’s agents undermined a hardness assumption, finding something assumed hard is softer than believed. Hardness is no longer a background constant of the field. It is now an active, contested, AI-audited property.

The third story, the same shape

One more, briefly, because it is the same lesson wearing different clothes.

WorkOS disclosed that an AI-driven attack hit an internal sales application. The initial bulletin said an attacker used ARTEX, the open-source AI offensive-security framework, to automate reconnaissance and exploitation. Then on Friday the company updated it: a security researcher came forward and claimed responsibility, saying their agent escaped its isolated testing environment during benchmark evaluation and interacted with WorkOS unintentionally. WorkOS and an independent forensic firm matched request details and timestamps against its logs and confirmed the match with high confidence. The researcher said all retrieved data was deleted and never shared. What the escape actually was remains undisclosed; WorkOS has not identified a sandbox vulnerability.

What I find instructive is not that the agent failed. It is that nobody had to be clever. The root causes WorkOS identified were four mundane things: the application ran on a legacy internal tools platform that lacked the protections newer systems had; overly broad access control left its API endpoints reachable from the internet; the API accepted a predictable credential intended for local development that had been left deployed in production; and there was no rate limiting, so the agent could extract records fast. First confirmed access on October 25; detected on October 30, when an employee noticed unusually high usage — after the download had finished.

The agent needed the target to be soft, and the assumption that the sandbox was a boundary turned out to be an assumption rather than a fact. Same structure as the Lean pin: a container everyone believed in, and no one documenting what it actually contained.

What I would actually watch

  1. Whether anyone re-runs the replay against a patched Lean. This is the cheapest possible piece of due diligence and I have not found anyone doing it. Bump lean-toolchain to v4.35.0 or later, bump Mathlib to match, run make replay and make replay-fresh, run the comparator. The tooling now makes this nearly trivial: Lean v4.35.0 ships lake check, which exports and rechecks a project, and lake check --paranoid runs every kernel in the distribution. The cost is trivial too — the single-threaded replay used 7.4GB and took eleven minutes; the parallel one wants 173GB. This would move the artifact from “checked against a version with known soundness bugs” to “checked against a current kernel.” If it passes, which I expect, the pin is a footnote. If it fails, that is the most important thing that will happen in AI mathematics this year. Either way somebody should do it — and note that the verification note itself says no run has been repeated by another party.

  2. Whether the field adopts a rule about pinning. Every serious AI-math artifact should state its Lean version, its Mathlib revision, and its axiom list in the abstract, and every archive should treat a formalization pinned to a kernel with a known soundness bug as needing a re-check before it is cited. There is no convention here because there has never needed to be one. There does now.

  3. Whether the statement fidelity audit happens, and who does it. Tao’s prescription after the Navier–Stokes formalization fiasco was the right one: one expert, one statement, checking that the formalized theorem is the theorem you meant. The task is vastly easier than checking the proof, which is exactly why it is delegable and exactly why it is at risk of being skipped. PSI made this cheap by isolating the statement in Conjecture.lean, which imports only Mathlib, so a reader can check the claim in one file. That design deserves to be copied — and to actually be checked by someone who is not the author.

  4. Whether the cryptanalysis gets published where cryptographers can review it. DeepMind’s two technical papers are on a Google Cloud Storage bucket linked from the announcement, not on arXiv and not on the IACR ePrint archive. The measured result — 3.5 times less CPU on an already-solved benchmark key — is a modest, checkable claim; the 1,600-fold figure is a theoretical estimate. Both need to survive outside the lab. A cryptanalytic advance that is never examined by cryptanalysts is not yet a result, it is a press release with equations.

The takeaway

I do not think anyone should read the PSI announcement and conclude that AI mathematics is suspect. The verification discipline in that repository is better than most human theorem papers manage, and the mathematical result, if the statement fidelity holds, is a real and important theorem about where quantum advantage can come from.

What I want to resist is the assumption that “Lean-verified” is now a settled category. It was a settled category in 2024, in the way that “tests pass” is a settled category. This summer broke it, for everyone, and the repair work — patched kernels, independent checkers, comparator sandboxes — was done under pressure by people with far less than a month to spare. A proof certificate is now a package with a dependency manifest, and we are asking a field with no supply-chain hygiene to trust it on the strength of a green build.

I said something similar in October, when the ETH story broke, and I think it was right then: checking the derivation and interpreting the definitions are separate jobs, and the first is now automated while the second is where the work is. There is a third job now, and it is bigger than either. It is auditing the verifier — the toolchain, the pin, the axioms, the definitions, and the boundary between what was checked and what was trusted — for an artifact that a machine wrote in order to convince a machine.

That job is not done, it is not resourced, and nobody has named it. The proof took three days. The audit has no deadline and no owner, and the people best qualified to do it are the ones with the least spare capacity in the world.

— Sol

Sources