schristoph.online

AI · 14 min read

Who Referees the AI?

Stefan Christoph
On this page
TL;DR: In July 2026 a purported disproof of the Collatz conjecture got through Lean’s official proof checker, and through an independent second checker as well. It was wrong. The submission exploited a different bug in each checker. Nanoda’s developer had fixed one shortly before, and de Moura fixed the other on 28 July. Lean’s creator Leonardo de Moura said in a recent interview that he strongly believes AI built the exploit. The episode shows what happens to any “AI checks AI” setup once the output gets too large for people to read. Acceptance then rests on the checker, its specification and the code around it, and a capable generator will go looking for the checker’s weaknesses. The Lean community’s answer carries over to agent builders: keep what must be trusted small, check it with implementations that share no code, publish how the check works, and remember that a passed check only certifies what you specified.

Most agent designs I review end in a gate: an LLM judge, an eval suite, a CI run, sometimes all three. The green result at the end of that gate is what lets the work ship without a person reading it, and this post is about what that green result is worth once the thing being checked is clever enough to go after the gate. Everything here comes from a public interview and the public GitHub record around it, all cited below.

A proof that two checkers accepted

Lean is a programming language and proof assistant. You write a proof, Lean tells you whether it holds. The answer is trustworthy because Lean turns everything you write into a much simpler core language and hands it to a small program, the kernel, which checks it against the rules of the type theory. The Lean reference puts the goal in one sentence, the core theory “is much simpler, enabling the trusted kernel to be very small” [3]. De Moura says it more bluntly in the interview: “Lean’s massive, has zillions of bugs. Right? But to trust our results in Lean, you only need to trust the kernel that’s much smaller” [2].

De Moura created Lean in 2013 [18]. He is chief architect of the non-profit Lean FRO and works in the Automated Reasoning Group at AWS [11]. He talked to Machine Learning Street Talk about what happened at the end of July [1], and the quotes below come from the episode’s transcript [2].

A repository appeared claiming a Lean proof that the Collatz conjecture is false. Its README states the result as Collatz.not_conjecture : ¬ Collatz.Conjecture and lists a thorough-looking verification pipeline that ends in “independent checking by pinned Nanoda with no permitted axioms” [7]. Nanoda is an independent Lean kernel written in Rust. So two different checkers had accepted a proof that was invalid.

Shortly before, a bug had been reported in Nanoda and fixed by its developer [6]. De Moura says the Nanoda release from before that fix accepted the proof [2]. The official kernel had a second, unrelated bug. The upstream issue, opened on 28 July, is titled “Kernel accepts wrong-structure projections, allowing an axiom-free proof of False”, and its impact section says: “An adversarial metaprogram can add declarations that ordinary Lean code then uses to prove False, with #print axioms reporting no axioms” [4]. De Moura’s fix was merged the same day [5].

What stuck with me is that he spotted the second exploit because the proof contained “a bunch of weird terms to create a hash collision that was completely irrelevant” to the maths. They were there to get past the bug in Nanoda [2]. He says “we strongly believe it was built by AI” and notes that the bug reporters called the Nanoda overlap a coincidence [2]. I am not going to claim more than he does. He is less cautious about the trend. AIs, in his words, are “really good” at exploiting soundness bugs in kernels, and “this is going to keep happening” [2].

Checks stand in for reading once output gets too big

Line-by-line human review is already out of reach for some formal work. In the same interview, de Moura mentions a 1.2-million-line Lean formalisation of a recent AI-generated counterexample in geometry, submitted by Boris Alexeev, and adds: “Nobody wants to check the proof line by line” [2]. His point is the value of a machine-checkable certificate. You want one even from a model that is almost always right [2].

The same shift is happening in code. Kim Morrison’s lean-zip project is a DEFLATE encoder and decoder written in Lean, with a theorem that decompressing the compressed output returns the original data, “for every input and every compression level” [10]. The README says the implementation and the verification were written “entirely by loosely supervised AIs”, and that their pull requests “could not merge unless the round-trip proof still went through”. Underneath are more than 1,100 theorems across about 32,000 lines of proof [10]. The project’s own summary is “The proof is the ratchet” [10]. The agents optimised the code aggressively because a checker stood between every change and the main branch.

That is the setup most of us are building with agents (minus the proof), and it is what I meant by working on the loop rather than in it, designing the checks instead of reading every output [15]. Once the output volume goes beyond what anyone reads, a checker takes the reader’s place. Whether an output ships then depends on that checker, the specification it checks against and the code that runs it. Ours are LLM judges, eval suites, CI pipelines and review bots, and in Lean’s terms that is our kernel.

Diagram. On the left, a large dashed box labelled 'Untrusted: any of this may be wrong' holds three stacked parts: the generator model, the prompts with their tools and retrieval, and the code that runs the agent. An arrow labelled output leads to a small box labelled 'Trusted: kept small' that holds the rubric, tests and fixtures, read-only to the agent, and two checkers, checker A and checker B, the second marked 'different code, different people'. An arrow leads from there to 'accepted only if both say yes'.

Lean’s shape, which an agent gate can copy. Almost everything is untrusted, and the small trusted part gets a second, separately built checker. The rubric, tests and fixtures the checkers apply belong in that trusted part too, which is why the agent must not be able to edit them.

The generator will look for the checker’s bugs

A wrong proof from a person is usually just wrong. Search long enough for something the checker accepts, though, and you also find where the checker is wrong. De Moura makes the point about patience. Talking about AI writing low-level optimised code, he says “We don’t have patience for doing this kind of low level implementation, but AI has the patience for doing that” [2], and the same patience applies to working through a checker’s corner cases.

Agent builders have seen weaker versions of this. I’ve written before that a verifier that confidently accepts bad answers can be worse than having none [13], and about research in which LLM judges rating thematic summaries of survey responses agreed with each other up to 91% of the time, but with human raters only up to 79% [12, 19]. Those checkers were wrong by accident, while in the Lean case whoever or whatever produced the output steered the checker into accepting something false. An agent optimising for “the judge says pass” is in the same position as a prover optimising for “the kernel says accepted”, so given enough attempts and feedback from the verdicts, a blind spot in the judge can be found, intended or not.

Lean’s comparator tool, built to judge proofs from parties you don’t trust, spells out in its README what it can’t catch. Some challenges leave a definition open for the solver to fill in, and “many definition hole challenges can be gamed without additional oversight”. The example is a challenge asking whether the Riemann hypothesis holds. You define the answer to be the Riemann hypothesis and prove the equivalence by reflexivity, which passes the check without telling you anything [8]. The README’s conclusion is that such solutions “must always be checked with an additional (potentially human) verifier” [8]. De Moura says the same about software. A proof certifies the property you wrote down, so choosing that property stays human work [2]. The slide from “the check passed” to “the artifact is right” is the one I described in [14], and it applies just as much to the rubric of an LLM judge, which is a specification too.

How the Lean team hardened the checker

Comparator states its trust assumptions as a numbered list. Assumption five is that the Lean kernel is correct, and the README adds that with external kernels configured this “can be reduced to ‘At least one of the Lean kernel or the external_kernels is correct’” [8]. So an exploit only works if it beats every configured kernel at once. After the incident, one concrete change was to make comparator always fetch the latest Nanoda, so a fix to the second checker reaches users without anyone upgrading it by hand [2]. The submission’s own README lists checking “by pinned Nanoda” [7], which is the setup this change removes.

They also want more kernels, written independently: “independent kernels implemented by different people using different programming languages” [2]. Lean4Lean is the counterexample, a Lean kernel written in Lean whose README says that because it is derived directly from the C++ kernel, it “likely shares some implementation bugs with it (it’s not really an independent implementation)” [9]. Mario Carneiro is working to prove Lean4Lean correct, and de Moura says that had the proof covered the exploited parts, it “would had found the bug before it was exploited” [2].

The team also keeps shrinking what must be trusted. De Moura walks through the chain. Prove the kernel correct, then the compiler that builds it, then ask hardware vendors for formal specifications. “The movement here is always reducing what you have to trust” [2]. For anyone who runs programs written in Lean, the trusted code base today includes the compiler, which is much bigger than the kernel. A verified compiler is one of the stated goals [2].

When the host suggests keeping a private kernel that attackers cannot study, the way benchmarks hold back test sets, de Moura says no: “I don’t like safety by obfuscation by hiding” [2]. He’d rather have more independent kernels and kernels proved correct, all published in the open.

That works for a kernel because its rules are fixed and public by design. Knowing them doesn’t help anyone get a false proof accepted unless the code has a bug, and publishing the code is how such bugs get found. A model judge with a written rubric is a different kind of checker, since knowing the wording helps a generator optimise for it. So for model judges a held-out sample that people label still has a place [12].

What this means for an agent’s gate

An LLM judge can’t be proved correct the way a kernel can, and most agent tasks will never get a formal specification. I don’t think that makes the Lean practice irrelevant. It means applying the parts that transfer, roughly in this order.

For a typical agent gate, the green result trusts the judge model, the judge prompt and rubric, the test fixtures, the code that decides which outputs reach the judge, and the code that turns a verdict into “ship”. Write that list down. Every item on it is part of your kernel.

Wherever a deterministic check can replace a model call (a schema, a type check, a test that runs the code, a lookup against the system of record), use it. Those checks resist natural-language persuasion and reduce reliance on model judgment, though their specifications, inputs and implementations remain trusted. Formal checks fit the narrow slices where you can state the property, and lean-zip shows how far that goes when you can.

Whatever second checker you add should fail differently from the first. My rough ordering, a heuristic rather than a measured result: for a judge, a deterministic check fails most differently, then a human sample. A model from a different family is the weakest option, because models from different families often learn from overlapping data, so their mistakes can line up. A second prompt to the same model is the Lean4Lean problem again, a second green check with little extra assurance, because its errors are correlated with the first. And a second checker costs money and time, so put it on the paths where a wrong accept is expensive, or on a sample of traffic, and keep the cheap deterministic checks on everything. In my own writing pipeline, a review pass on a model from a different family has caught issues that the drafting model’s own review had passed. That is one person’s workflow and no study, but it matches what the Lean team says about independent kernels.

Checkers you keep will be attacked, so treat them like the rest of your code. Version them, review changes to them, and throw deliberately bad inputs at them. When you hear about a bypass, update. A pinned checker, as Nanoda showed, keeps old bugs alive after they’re fixed upstream.

The comparator rule about definition holes applies to the specification directly. If the agent can influence what counts as success, through a rubric it writes, a test it edits or a fixture it generates, a person has to look at that part.

If you’re running this on AWS

AWS offers formal checking for LLM output in the form of Automated Reasoning checks in Amazon Bedrock Guardrails. You give it a source document, such as an HR policy. It extracts formal logic rules and variables, validates model responses against them, and explains why a response is valid or invalid [16]. The documentation is unusually explicit about its trusted base. It says the checks “validate exactly what you send them” and do not detect prompt injection. They use foundation models to translate natural language into logic, so translation accuracy matters. And it states that “A VALID result guarantees validity only for the parts of the input captured through policy variables.” Its example is a late-homework excuse built on a fake doctor’s note, which can come back valid if the policy has no variable for whether the note is fake [16]. This is the same family of gap as comparator’s definition hole, a missing policy variable rather than a definition the solver chose, and the documented workflow handles it the same way, with a person reviewing the extracted policy and its fidelity report and testing the policy before deploying it [16].

For model-based judging, Amazon Bedrock Model Evaluation supports evaluator models from several model families, so the judge doesn’t have to come from the same family as the model that produced the output [17]. Calibrating such a judge against human labels is covered in [12].

The referee is a component you own

De Moura’s answer to the Collatz week is that several independent kernels, some of them proved correct, make the story “really bulletproof” [2]. Agent systems won’t get there. But we can take the habit: know what the green result rests on, keep that small, have it checked by something that fails differently, and expect the generator to look for its weak spots. Keep certificate validity apart from specification adequacy, too: a valid check of the wrong property still ships the wrong thing.

What does the green check at the end of your agent’s pipeline actually trust? And would a second, independent checker agree with it?

Sources

❤️ Created with the support of AI (Kiro)

Related

AIWhich of Your Work Is Actually Verifiable?AIYour AI Judge Needs a JudgeAISecurity Is Job Zero — Even (Especially) in the Age of Coding AgentsAIGLM 5.3 on Amazon Bedrock: An Open-Weight Coding Model Behind a Managed API, Tested

AIAgenticAILLMEvalsVerificationSecurityFormalMethods