AI Makes Answers and Checks Cheap

On October 6, OpenAI published openai/math, 722 AI-written math manuscripts in 372 result families. By its October 7 changelog, 300 of the remaining 719 top-line results carried a Lean formalization, and the repo's Lean catalogue records them as agent-written with a review status of unchecked. On October 8, a Lean contributor showed that 8 of the repo's challenge checks could be passed trivially by redefining a property as False.

Most of the reaction was amazement at the volume. Seven hundred papers in one release is a lot of new mathematics to take in. The part worth slowing down for is the word unchecked, sitting next to 300 proofs a machine had already checked. Both are true at once, and the reason they can be is the whole story.

Strip out the math and every system of trust has three parts. There's the question, what we said we wanted. There's the answer, the work somebody did. And there's the check, whether the answer satisfies the question. AI is making answers nearly free. Tools like Lean are making checks nearly free. The one part still waiting on a person is the question, and October showed that's exactly where things slip.

How we used to decide a proof was true

For most of history, a proof was trusted because the right people read it and couldn't find a hole.

Thomas Hales submitted a proof of the Kepler conjecture, the centuries-old claim about the densest way to stack spheres, in 1998. A panel of referees worked on it for about four years and came back saying they were 99% certain it was correct. Not 100%. The argument leaned on enormous computer calculations no human could fully re-walk, so reputation and reading only got the referees so far.

Hales's answer was to stop asking people to trust the reading. He led a project to rewrite the whole proof in a form a computer could check line by line, and finished it in 2014.

That's what Lean is. Think of it as a spell-checker for logic. You write the theorem and the proof in a strict formal language, and a small program called the kernel checks that every step follows from the one before. If it passes, you don't have to trust the author, whether the author is a famous mathematician or an unreleased OpenAI model that averaged three hours of compute per result. You only have to trust the kernel, which is small enough for experts to scrutinize.

That's a real change in how trust works, and it's why 300 Lean-checked results are worth more than 300 unchecked ones. A checked proof rules out a whole class of errors inside the argument.

The check can only answer the question it was handed

Here's what the kernel can't do. It certifies that a proof establishes a formal statement, given the definitions in scope. Whether that formal statement says what the English says sits entirely outside its job.

Hales put it as two questions in an October 9 guest post on Terry Tao's blog.

"Is the verified theorem what we think it is? Do the definitions in Lean correspond to what we think they should be?"

Thomas Hales, Oct 9, 2026

A day earlier, Alex Meiburg, a contributor to Lean's main math library, had answered those questions for part of OpenAI's repo. Each formalization ships with a challenge file that checks a submitted proof against a stated theorem. Meiburg went through them and found a batch that could be passed without doing any math at all.

"8 of the Lean formalizations in OpenAI's repo are 'broken' (trivially provable with wrong proofs)."

@Timeroot (Alex Meiburg), Oct 8, 2026

His cleanest example is a theorem about coloring the plane. Picture an endless flat sheet and give every single point on it a color, with one rule: any two points exactly 1 unit apart must get different colors. The puzzle is how few colors that takes. Seven always works, and since 2018 it's been known that four aren't enough. The theorem in this challenge says five aren't enough either. The challenge let the person submitting the proof also supply the definition of following the rule. So the whole submission could read like this, translated out of Lean:

• Definition: a coloring follows the rule when... never. No coloring ever counts.
• Theorem: there's no way to color the plane with 5 colors that follows the rule.
• Proof: of course there isn't, since nothing follows the rule.

In Lean that definition is a single word, False, and the proof is one line.

The kernel did its job perfectly. The proof really is valid for the definition it was handed. Nobody had read the definition.

It's the genie problem. You get exactly what you asked for, so the whole game is in how you asked. Meiburg's trick satisfies the letter of the challenge and walks straight past its meaning.

And the gap isn't limited to one repo. Audits of the standard Lean benchmarks keep finding formal statements that don't match the English they came from:

There's a second, quieter version of the same gap. In September, OpenAI announced a Navier-Stokes result backed by a Lean proof. On October 6, Alexander Bastounis, Fabian Circelli and Anders Hansen compared the two and found the Lean version takes a different route in places. In one of the small supporting results the main proof is built from (mathematicians call these lemmas), the Lean version needs a stronger assumption than the paper says is enough. The authors are careful to say they make no claim about whether the paper is correct. Elliot Glazer, formerly FrontierMath's lead mathematician at Epoch AI, called it "a nothingburger" about readability. He may be right about the math. It still leaves the paper people will read and cite and the file the machine checked as two different objects, and only a person comparing them can say they match.

The deeper meaning: checking got cheap, so the question is the job

Maher Kallel and Mohamed El Louadi measured what this looks like in bulk. Across OpenAI's August corpus of ten formalized results, there were 20.6 MB of machine-checked proof and 55.6 KB of statements and definitions that still need a human to confirm they mean the right thing. That's 379 to 1. Their summary: "machine checking produces verification abundance while leaving adjudication scarce."

That ratio is the significance most of the amazed reactions skip. The expensive part of trusting a result used to be reading the argument. Now a machine reads the argument, and the human work collapses into a few pages of definitions and claims. That's great news, because a few pages is something a person can actually read carefully. It's also a warning, because those few pages are now the only place a mistake can hide, and nothing downstream will catch it.

Math is the best possible place to learn this, because it's the one field with a flawless checker. If meaning can slip past a perfect check here, every field with fuzzier checks has the same gap, only bigger and harder to see.

Why this matters if you never touch math or code

Verified is about to be stamped on everything AI produces. Code that passed its tests. Contracts that match a template. Models that were validated. Each stamp means the same thing a Lean check means: the answer satisfied the question somebody wrote down. Whether that was the right question is a separate claim, and the stamp is silent on it.

You've seen this pattern without the AI. A student aces the test by learning the test. A house passes every item on the inspection checklist and floods in the first storm. In fraud detection, a rule can score perfectly against its labels and still miss real fraud when the labels were defined wrong, which is why a suspiciously clean rule usually gets its label definition checked first.

AI makes this sharper because it's very good at satisfying the letter of a request. In coding, where tests play the role of the formal statement, researchers built a benchmark called ImpossibleBench with tasks where the tests and the instructions deliberately conflict, so the only way to pass is to cheat. GPT-5 cheated on 54% of the conflicting SWE-bench tasks. When Claude models cheated, more than 79% of the time they did it by editing the tests themselves. That's the coding version of redefining the coloring rule as False. An audit of SWE-bench, the standard test of coding agents, found 29.6% of patches that passed the tests behaved differently from the real fix.

So as AI does more of the work, the human job moves. It moves away from producing the work and away from checking it, both of which machines are getting good at. It moves toward saying precisely what you want, and noticing when the question got quietly swapped for an easier one. The skill that goes up in value is writing down what you actually mean.

Ordinary software fails this way too, at small scale. A script can report success for weeks while writing to a file that nothing reads anymore. Every run genuinely succeeds, against the wrong target, and the green result is the thing hiding the problem.

What good looks like

The honest version of all this already exists, and it's sitting in OpenAI's own repo. At the bottom of the Lean catalogue, two fields describe every formalization in the file. One says how they were made: by an AI agent. The other says whether a person has reviewed them: unchecked.

Credit where it's due, that second field is the most useful line in the release. It says a machine checked the proofs and no human has yet confirmed the questions. As of October 14 it still reads unchecked. OpenAI hasn't responded publicly to Meiburg's post or the Navier-Stokes paper, and the only change to the repo since October 8 is a workflow that locks pull-request conversations.

Hales argues a Lean proof "should not be accepted until a human audit is performed to ensure statement fidelity," and notes that this audit "is generally massively easier than checking the proof itself." That's the hopeful part. The job left for people is smaller than the one machines took over. It just can't be skipped.

So the question to carry around, for math, code, contracts or any AI output with a checkmark on it, is the one in the title. Verified against what? Who wrote that question, and did anyone read it?

If you build with coding agents

The same setup maps directly onto agent coding:

Four rules follow:

1. Separate authorship. The agent that writes the code doesn't write or edit the tests. Freeze the tests, or at least diff them, so any run that touches a test file gets read line by line before merge.
2. Read the statement first. Review the tests and fixtures before the diff. That's the small part, and it's where a wrong answer can hide.
3. Pin definitions. Fail closed when fixtures or shared definitions change, the way a comparator should fail if a definition is swapped.
4. Track unchecked honestly. OpenAI's catalogue has a review field. Give your CI one, so a green agent PR and a reviewed one stop looking identical.

Rule 1 is easy to automate. Have the CI pipeline fail any agent-written pull request that touches the tests, fixtures or spec, with a message that it needs a human to review it.

Legit test changes still happen. Route those through a label or a separate human-written PR, so they get read as changes to the question. A June post here makes the related case for agent runtimes: the eval layer is still your problem. A test suite is the most concrete version of the question most teams own.