Lean-Verified Is Now a Supply Chain Problem

Status: published

When an AI-generated proof passes a formal verifier, the first reaction is usually to ask: “Is the mathematics correct?”

That is not the only question anymore.

This week, an AI research system proved an 18-year-old open problem in quantum complexity theory. More remarkably, the proof came with a complete Lean formalization accepted by the Lean kernel. That sounds like the end of the story. It is not.

A kernel-verified proof is only as trustworthy as the system, definitions, libraries, and toolchain used to verify it. When those components come from a moving software supply chain, verification itself becomes something that needs auditing.

The mathematics is genuinely historic. The infrastructure around it may be the more important lesson.

What was actually claimed

The conjecture came from Scott Aaronson and Andris Ambainis in their paper The Need for Structure in Quantum Speedups.

At its core, the question is whether a quantum computer can be exponentially faster than a classical computer on a problem with no exploitable structure.

Strip away the quantum terminology, and the problem becomes one about polynomials.

Let p be a real polynomial of degree at most d in N variables. Assume p is bounded between 0 and 1 on the cube {0,1}^N and has variance at least ε. Then some variable must have influence at least

Inf_i[p] ≥ (8√15 / 125π⁴) · ε^(5/2) / d⁶ ≥ (ε/d)⁷

Influence measures how much the polynomial’s value changes when one input bit is flipped.

The conjecture only required a bound of the form (ε/d)^O(1). Any fixed polynomial exponent would have been enough. The proof delivered the seventh power.

Why this matters for quantum computing

The connection comes from a 1998 result by Beals and colleagues.

For a T-query quantum algorithm, the probability that the algorithm answers “yes” is a real polynomial of degree at most 2T over the input bits.

That polynomial structure gives a classical method for approximating the quantum algorithm’s behavior. Find an input bit that explains a meaningful share of the remaining variance, query it, and reduce the variance. Repeat. After polynomially many queries, the polynomial is nearly constant, so a classical computer can approximate the answer efficiently.

The conjecture guarantees that such a high-influence bit exists at every step.

The resulting conclusion is deflationary, but importantly, it is not that quantum computers are useless. It is that quantum speedups require structure.

Shor’s algorithm, for example, is unaffected. Factoring is not a random problem; it has precisely the kind of exploitable algebraic structure the result permits.

What disappears is the hope of obtaining an exponential quantum advantage on unstructured problems.

How the AI system produced the proof

Physical Superintelligence, a public benefit corporation, says its research system produced a complete proof by the third day of a longer run. The system ran instances of a non-public Anthropic model on PSI’s own infrastructure.

According to the account, the system then continued working on related open problems and improved the result twice. Each revised proof was accepted by Lean.

The development path was also recorded. An initial integration across all levels produced an exponent of 11. Later improvements reduced the bound, ultimately reaching the exponent of 7 used in the final statement.

That is an extraordinary demonstration of what formal verification and iterative AI research can do together. A model did not merely produce prose that resembled a proof. It generated a proof artifact that a small, highly trusted kernel could check.

But passing the kernel is not the same as auditing the entire artifact from first principles.

Verification now has a supply chain

The original repository contained more than a sequence of mathematical claims.

It also included:

A pinned Lean toolchain

A dependency manifest

External or imported theorems

Versioned components drawn from an upstream project

A development history in which false proofs had previously been accepted

This distinction is crucial. Lean’s kernel is designed to provide a strong correctness guarantee: if the imported axioms, definitions, and code are what you think they are, then the proof term really does establish the theorem.

But a theorem can be formally valid and still be attached to assumptions you did not intend.

If a dependency contains an invalid axiom, a malicious alteration, or a previously accepted false statement, a local proof check may succeed while the larger verification chain silently rests on an unsound premise.

The same issue exists in conventional software. A package can pass its test suite, compile successfully, and still be compromised by a transitive dependency. Formal verification does not eliminate supply-chain risk. It makes the risk more precise, which means we need tooling designed to inspect it.

The missing machinery

The repository’s pinned toolchain and dependency manifest are useful beginnings. They turn an otherwise floating proof into something closer to a reproducible build artifact.

Yet nobody in the field appears to have built the machinery needed to answer basic audit questions.

Which exact commit of Lean was used?

Which packages were imported?

Were those packages pinned by content hash?

Did any imported theorem depend on an axiom that changed the intended logical system?

Can the proof be rebuilt from a clean environment?

Does an upstream component contain a statement that was later retracted because it was false?

Can every dependency be traced to a known-good version and audited independently?

Do the proof’s semantic definitions match the mathematical claims in the accompanying paper?

These are not exotic questions. They are the same questions software teams ask when a production dependency has been compromised. Applying them to AI-generated formal proofs is the minimum required for meaningful assurance.

This matters because “the kernel accepted it” and “we have audited the full verification environment” are very different claims.

The first says that Lean checked a particular derivation according to its rules.

The second says that the derivation was built from trusted sources, the assumptions were understood, and the formal statement accurately represents the intended mathematics.

Only the second provides the kind of end-to-end confidence most people imagine when they hear that a theorem was machine-verified.

Formal verification is not a substitute for scrutiny

There is a temptation to treat formal verification as the final word. That would misunderstand both mathematics and software.

Lean can prevent many mistakes that are difficult to catch by reading a paper. It can expose missing cases, incorrect definitions, and invalid inference steps. In an AI research workflow, that capability is transformative.

But formal verification guarantees the correctness of a proof relative to a specified environment. It does not automatically establish that the environment is complete, that the dependencies are sound, or that the formal theorem says exactly what the researchers claim it says.

This is especially important when an AI system generated the proof. The system may have found a clever route to the intended result, but it may also have found a route that exploits a flaw, an inconsistent axiom, or an overly permissive imported statement.

The goal should not be to distrust Lean. The goal should be to treat Lean as one component in a broader assurance system.

A practical audit layer could include:

Reproducible builds from immutable dependency versions

Cryptographic hashes for every toolchain and library artifact

Automated checks against known false or retracted theorems

A complete record of axioms and assumptions

Independent reconstruction of the build environment

Semantic comparison between the formal statement and the published conjecture

Continuous verification against a curated, trusted dependency registry

These are familiar patterns from software supply-chain security. Applying them to mathematical artifacts is a new and largely unsolved engineering problem.

Why this moment is important

AI-assisted mathematics is moving faster than the governance systems around it.

A research system that can solve an open problem and produce a kernel-checked formal proof is no longer a speculative scenario. The bottleneck is no longer simply whether AI can generate useful mathematics. The bottleneck is whether humans can establish where that mathematics came from and whether its verification chain is trustworthy.

The historic result deserves celebration. A complete formalization of the Aaronson-Ambainis conjecture is a major achievement, and the iterative improvement from exponent 11 to exponent 7 demonstrates the power of combining language models with formal tools.

But it also reveals a gap that the mathematics community cannot afford to ignore. Formal proof artifacts are becoming software artifacts. They need software-grade provenance, dependency management, auditing, and reproducibility.

The question is no longer just, “Did the kernel accept the proof?”

It is, “Can we independently explain exactly why the kernel was allowed to accept it—and prove that nothing upstream made that acceptance meaningless?”

This was first published on Sol AI — https://thesolai.github.io