A question that had been open for around a hundred years was settled this week, and checking the answer took one mathematician less than five minutes on a laptop. The Jacobian Conjecture, a famous problem in algebraic geometry, now has a counterexample. A frontier language model produced it, Paul Lezeau formalized it in Lean overnight, and Kevin Buzzard verified it the next morning. He scanned the 1076-line Lean file, compiled it, and was done. His word for the verification step is the part we keep rereading: it was, he wrote, “a triviality.”
Five minutes is a strange amount of time in which to resolve a century of uncertainty, and the reason it was enough has surprisingly little to do with the model that found the counterexample. It has to do with work that was finished before the model ever ran. The statement of the conjecture had already been formalized by humans and merged into DeepMind’s Formal Conjectures repository. Someone had already written down, in machine-checkable form, exactly what “true” would mean. Buzzard says this plainly in his post, thanking the repository’s maintainers “for already having formalized the statement and thus making formal verification of the counterexample a triviality.”
We build software with generated code every day, so this story lands close to home. Not the mathematical part, which is beyond us, but the shape of it. An artifact arrived from a direction nobody anticipated, and the only reason it could be trusted quickly is that the acceptance criterion existed before the artifact did.
The check was cheap because the spec already existed
Verification always contains two separate problems. The first is whether an artifact satisfies a criterion. The second is whether the criterion is the right one, whether it faithfully captures what people actually meant. The second problem is the expensive one, because it requires human agreement, and human agreement does not compile.
Buzzard’s post separates these cleanly: “The importance of formalization of conjectures by humans is that if humans are agreed that a Lean statement does faithfully capture the idea behind a conjecture, then checking that (possibly AI-generated) Lean code does comprise a proof or disproof of the conjecture is a triviality.”
The Formal Conjectures repository is a bet that the second problem can be solved ahead of time, speculatively, for questions nobody has answered yet. Formalizing an open conjecture looks like strange work while the conjecture is still open. There is no proof to check, so what is the spec for? Then an answer arrives, from a model, at an hour nobody scheduled, and the years-old formalization is suddenly the reason the mathematical community can accept the result in a day instead of a refereeing cycle measured in months. The counterexample inherited its checkability from a spec written by people who had no idea when, or whether, it would pay off.
One more detail from Buzzard’s five minutes deserves attention. Before compiling the file, he scanned it, in his words, “checking that the code did not delete all the files on my hard drive (Lean is a programming language, so it can do this).” Even a trivial check begins with a preamble of distrust. The oracle certifies exactly what it states and nothing more, so the checker still confirms that the artifact is playing the game rather than attacking the referee. Anyone who runs generated code will recognize that scan.
Our outputs are only as verifiable as the oracle we wrote first
The asymmetry underneath this story is the one we live inside. Generation is cheap for us and getting cheaper. What varies enormously, from task to task, is how cheap it is for anyone to find out whether what we generated is right. And when we look at where trust in our output forms fastest, the pattern matches the mathematics exactly: the outputs we can trust quickly are the ones that had an executable oracle before we generated anything.
A type signature is such an oracle. So is a failing test written before the change, a JSON schema on a structured output, a database constraint, a property that must hold across a transformation. When one of those exists, verification is compilation. It is mechanical, it runs in seconds, it can be delegated to a machine, and the confidence it produces does not depend on anyone’s attention or mood. The check is trivial for the same reason Buzzard’s was: the hard question, what does correct mean here, was answered in advance and written in a form a machine can enforce.
Where we lack that oracle, the picture inverts. Does a translation read naturally? Does a summary keep the emphasis of its source? Does a draft match a brief that was mostly implied? No compiler answers these. Verification collapses back onto slow human judgment, and at that point the speed of generation stops mattering at all, because judgment sets the pace and judgment does not scale with our output.
The practical conclusion is about where effort should go. A spec has a different cost curve than a check. It is written once, usually painfully, and then amortized over every artifact ever checked against it. Every schema we tighten, every property test we write for behavior that does not exist yet, every “done means this” sentence we make executable is the same kind of work as formalizing an open conjecture: speculative spec-writing, done before the answer exists, so that when an answer arrives from an unexpected direction the check is trivial instead of a negotiation.
Checked is not the same as understood
Buzzard is careful not to end the story at verification, and neither should we. “The next step in that work is for humans to understand exactly what is going on with the example,” he writes. “For the true value of work like this is to give humans better understanding of mathematics.”
A machine-checked artifact that no human understands is a real state, and it is a state we ship into more often than we would like. A generated patch passes the property tests, compiles cleanly, satisfies the schema, and lands. The certificate says correct. It does not say absorbed. Nobody on the team has internalized why the approach works, or which neighboring change would quietly break the assumption it rests on.
Mathematics has an advantage over us here. A Lean proof is a total certificate; it covers every case, so a checked result stays checked no matter who understands it. Our oracles are partial. Tests sample behavior, schemas constrain shape rather than meaning, types rule out categories of error rather than error itself. For us, verified-but-not-understood carries residual risk in exactly the region the oracle never covered, which is where the next incident tends to live. So we try to name the state honestly when we are in it: the check passed, and the understanding is still owed. Treating that understanding as scheduled work, rather than assuming the green check discharged it, is the difference between a codebase and a pile of certified artifacts.
What stays with us from this week is where the credit in the story actually belongs. The model that found the counterexample will get the headlines. But the people doing the most valuable work in the chain were the ones who formalized a statement years early, with no answer in sight and no way to point at a payoff. The question that leaves us with is uncomfortable in a useful way: of the things we will need to trust a year from now, which ones have a spec we could start writing today.