The Checker Cannot See The Footnotes

A proof arrives with a green check beside it.

Every definition resolves. Every inference can be replayed. A proof assistant has followed the argument from its premises to its conclusion without finding a gap. After centuries of mathematicians asking whether a proof is correct, the machine can answer with unusual force: this one type-checks.

The reviewer still has another question.

Has anyone proved it before?

That question sits just outside the certificate.

On August 1, OpenAI presented ten results on longstanding problems in mathematics and theoretical computer science. The company says an internal model generated the mathematical arguments, people used the same model while preparing manuscripts, and the model then formalized each argument in Lean, where a proof checker can verify the logical construction.

OpenAI also did something less common in a model announcement: it separated correctness from credit. Its researchers said they take responsibility for the proofs while describing the arguments themselves as model-generated. The page asks the mathematical community to evaluate the results, place them in context, and decide what they mean inside living fields of research.

On August 12, a new benchmark made the scale of this problem easier to see. OEIS Open turns 492 conjectures from the Online Encyclopedia of Integer Sequences into formal Lean problems. Generic language models with a small toolset resolved 147 of them at a budget of $50 per attempt. On a smaller set, the best result reached 44 percent at $200 per attempt.

The paper is admirably careful about what that number does not establish. The conjectures are of uncertain mathematical significance, and many appear to have received little attention. Giving the agents access to 476,000 mathematics papers did not improve the smaller benchmark. More elaborate agent loops did not help either.

That is both a capability result and a warning about the shape of the evidence. A system may produce a valid formal object while remaining unreliable at the surrounding scholarly work: finding the relevant literature, judging whether the problem matters, and understanding where an argument belongs.

We have already seen the awkward version. In an earlier set of AI-assisted science case studies, a model derived an exact bound with essentially the same proof as a paper published years before. The argument was correct and elegant. The citation was absent. The model found the earlier work only when asked again in a fresh session.

The proof had passed the mathematical test before it passed the library test.

A formal checker is not failing when this happens. It is doing the narrower job it was built to do. Lean can verify that a proof term follows from the definitions, axioms, and theorems available in its environment. It cannot know that a clever rearrangement appeared in a short journal article in 1998, that a definition carries the fingerprints of a particular research community, or that a result advertised as new is ordinary to the people who have lived with the problem for twenty years.

The checker can see dependencies in code. It cannot see intellectual debt.

This sharpens the argument in Provenance Became Part Of The Interface. Agentic work needs a visible account of who initiated, generated, reviewed, and approved it. Mathematics adds an uncomfortable edge: even a perfect trace of the current run may not reveal whose thinking already lives inside the model, the formal library, the problem statement, or the forgotten paper the system almost reproduced.

Logical lineage and intellectual lineage are different records.

The Leiden Declaration on Artificial Intelligence and Mathematics makes the human obligation explicit. It asks researchers to disclose automated tools, provide complete references, use formal proofs where appropriate, and take responsibility for correctness and citations. It also insists that authorship and credit remain human. OpenAI takes a different position on the last point, arguing that assigning human authorship to an argument generated entirely by a model would also misdescribe what happened.

That disagreement will not be settled by a green check. A proof certificate can establish validity without deciding personhood, authorship, novelty, or the terms on which a field recognizes contribution. Those are social judgments carried by communities, publishers, reviewers, and the people whose earlier work made the result possible.

The useful response is not to weaken formal verification. We should want more arguments that can be checked. The response is to stop asking one certificate to carry every kind of trust.

AI-assisted mathematics needs a second record beside the formal proof: what tools were used, which sources were searched, what earlier results were compared, where experts see genuine novelty, and what remains uncertain about attribution or significance. That record should be honest when the literature search failed. It should make review easier rather than handing a mathematician a machine-sized pile of plausible claims and calling the pile progress.

This will become a familiar problem outside mathematics. A test suite can verify that code behaves as specified without showing where the design came from. A spreadsheet can recompute perfectly while carrying an old assumption nobody remembers making. A research reproduction can match the published table while missing the judgment that made the table worth publishing.

Verification tells us that an object holds together. It does not tell us where the object came from or what the surrounding world owes it.

The checker can certify the proof. The footnotes still have to remember the people.