Skip to content
Vale, home

Proved, but Not Yet Understood

15 min read

On OpenAI’s 719 machine-written math manuscripts, a quarrel over who sets the norms, and what our code review queues have been trying to tell us about understanding.

On the night OpenAI put its mathematics repository on GitHub, the complexity theorist Dana Moshkovitz texted her husband about the manuscript claiming to prove the Unique Games Conjecture, a statement he says she has worked toward for as long as he’s known her. “It feels like something written by someone who’s on psychedelics,” she wrote. Her husband is Scott Aaronson, who quoted those texts in his post “The Mathocalypse”, just below a line I read a few times. The UGC manuscript comes with a Lean certificate, so a machine has checked the formal proof, and yet “it also appears that no human has understood just about any of these proofs yet; the race to do so has just started.”

My last post, Let the Agents Cook. Make Them Prove It., argued that verification is the foundation of agent autonomy, because machine-checkable evidence is what makes it reasonable to let agents do more on their own. I still believe that. Here, though, verification had apparently worked, and the people who cared most about the result were still standing outside it. So this post is a qualification rather than a retraction: verification can justify trusting an output without creating the understanding needed to extend or maintain it, and in software, where someone has to change the code again next quarter, that understanding is a large part of the job. The two ideas are complementary, and mathematics just happens to make the gap between them easier to see.

the short version of the release

On October 6, OpenAI announced “a broad range of new mathematical results produced by an internal frontier model” (unreleased), published as a GitHub repository of 719 manuscripts organized into 372 “families” of related results. By OpenAI’s account the average result used roughly three hours of ChatGPT Pro thinking compute, and after an October 7 update about 42% of top-line results are formalized in Lean, 300 of 719. All of it is self-reported and none of it peer-reviewed. One day after release the history file recorded three withdrawals because “a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers,” which anyone who has watched one bad utility function quietly break three services downstream will recognize.

A week earlier the Advisory Group on Mathematics and Artificial Intelligence, nine independent mathematicians including Timothy Gowers, Martin Hairer and Edward Witten, had published guidelines for responsible release of AI-generated mathematics. On release day the group issued a carefully neutral statement calling the release “the beginning, not the completion, of the process of human understanding.”

two different ledgers

I keep coming back to the process of human understanding, because it names something the word “verified” tends to swallow.

A Lean certificate answers a narrow and extremely valuable question: does this formal statement follow from these definitions and axioms, according to this kernel? Even that answer depends on the formal statement being the right one. In a guest post on Terence Tao’s blog, Thomas Hales argues that a Lean proof “should not be accepted until a human audit is performed to ensure statement fidelity,” and a preprint by Bastounis, Circelli and Hansen argues that an autoformalized proof can follow a different argument from the paper humans are reading. The deeper issue is that correctness and comprehension are kept on two separate ledgers, and a certificate only writes to the first one. Comprehension is what lets you reuse an idea, notice that it would also crack a neighboring problem, or see where it breaks if you change a hypothesis, and most of the value of a new result sits on that second ledger.

The advisory group’s guidelines state the old norm plainly: “the authors of a paper should understand the mathematical argument of that paper, have verified its correctness themselves, and take full responsibility for the content.” Read that with a pull request in mind. Understanding, verification and responsibility have always travelled together in the person of the author, so we rarely had to name them separately. Machine authorship pulls them apart, and once you can have verification without understanding, it’s no longer obvious who holds the responsibility.

the same bottleneck, in our repos

We’ve been running a version of this experiment in software for a while, just without the vocabulary. Harvard economists Fiona Chen and James Stratton used Jellyfish engineering analytics covering roughly 300 million work events across 718 firms, from January 2021 through March 2026. Their paper, covered by Ars Technica, finds agents raise lines of code by 30%, commits by 20% and pull requests by 23%, while resolved Jira issues and epics, the authors’ proxy for shipped software, show small, statistically insignificant changes. The time from opening a pull request to merging it rises 49%, the share of PRs where a reviewer formally requests changes nearly doubles, and comments per PR rise 35%.

I lead a web engineering team and still build a lot myself, so the review queue isn’t an abstraction for me (I touched on it in Agentic Engineering Is Not a Vibe). At its core, code review is the moment a second person builds enough of a mental model of a change to share responsibility for it. That’s comprehension work, and it doesn’t get faster because the code was cheaper to write.

An agent’s PR also tends to arrive without the thing a human author brings into review almost for free, which is someone who can answer why.

A colleague can usually explain an odd choice in a minute. With an agent’s change, the reviewer reconstructs the reason from the diff, or re-prompts and hopes to get the reason rather than a plausible story about it.

I suspect that reconstruction is where a good share of the extra review time goes, but that’s my hypothesis, not the study’s finding. Longer reviews don’t by themselves show that comprehension got harder. The same numbers could come from larger changes (lines of code grew faster than pull requests), from reviewers stretched across more of them, or from teams raising their standards, and the authors can’t fully separate more code arriving at fixed review capacity from review itself changing, “either because the code written now is of worse quality, or because the standards of code review have changed.” It’s also a job market paper, not yet peer-reviewed, that measures firm-level adoption rather than individual use, with data that stop before the latest generation of agents. So the study is consistent with a comprehension bottleneck without proving one. What it does show fairly convincingly is that the cost moved downstream, to wherever humans have to understand things.

a quarrel about who sets the norms

The sharpest reaction to the math release came from the Association for Human Mathematics, whose statement on the AHM site was reposted as a guest post on Tao’s blog, which he hosted but didn’t write, a distinction plenty of people missed. It calls the release “not a demonstration of scholarship, but a demonstration of power” and urges mathematicians to stop working with OpenAI. I don’t think a boycott helps, since it doesn’t un-prove anything, but in economic terms the complaint is fairly precise. Each result cost about three hours of model compute by OpenAI’s account, absorbing them will cost the receiving community years of skilled human attention, and the producer set the schedule. Cheap to produce and expensive to absorb is exactly the asymmetry sitting in our review queues.

The contrast Aaronson draws next is, for me, the most interesting part of his post. A day before OpenAI’s release, Josh Alman and Virginia Vassilevska Williams posted a preprint with truly subquadratic 3SUM and truly subcubic all-pairs shortest paths, refuting two long-standing hypotheses of fine-grained complexity. The paper says Claude discovered the core algorithm in a single session of 16 million output tokens “with no human input,” and that Anthropic shared it with the authors under a confidentiality agreement and offered compensation. The authors then “worked to understand, simplify, strengthen, and extend the algorithm,” wrote the paper, and “take full responsibility” for it, with the Lean certification done afterwards. Aaronson calls these the “OpenAI model” and the “Anthropic model” and is fair to both: the first “sets up a crazy race among humans to digest and explain a messy AI proof,” while the second “puts a private company in the position of picking and choosing which human mathematicians get to be the emissaries of the AI.”

Put in the terms of this post, the Anthropic model is comprehension-first, since the result reached the world already attached to two people who understood it and would answer for it, while the OpenAI model is verification-first, with comprehension left as an exercise for the reader. I don’t think either is obviously right, and it bothers me a little that both were chosen by companies rather than by the communities that have to live with them.

the firehose, with patches attached

The third story makes the pattern clearer, because here the receiving community asked for the firehose. On October 8, Anthropic launched OSS Scanner, an opt-in service whose vulnerability reports are “fully model-generated, without human review or triage,” because the company remains “bottlenecked on our human capacity to validate these findings.” Maintainers kept asking for everything anyway.

An independent analysis by Vulnerabilities.ai of Anthropic’s own disclosure dashboard, as of October 2, lays out the funnel: of 6,157 findings disclosed to maintainers, about 78% went directly without independent review, and 516 had been patched upstream. The disclosed count measures production. The patched count measures action taken: a fix landed upstream, which is real but lags. Neither measures comprehension. A maintainer can understand a finding perfectly well and still not patch it, because it duplicates a known issue or falls outside the project’s threat model (Anthropic’s glossary, the analysis notes, counts duplicates and “won’t fix” findings as true positives). Conversely, a ready-made patch can be merged without deep understanding once its reproducer stops reproducing, which is this post’s worry one level down. So 516 tells me how much of the output became changed code, not how much of it anyone understood.

Here’s the part I can’t stop turning over. In security it’s OpenAI running the curated model: its Patch the Planet initiative has Trail of Bits researchers “reproduce the evidence” and “reassess severity” before maintainers see anything, while Anthropic is the one sending raw output. In mathematics the roles are reversed. Whatever is driving these choices, then, it isn’t a stable corporate philosophy about openness. 🤔

My tentative explanation is that whether a firehose is tolerable depends on the distance between the new artifact and what the receiver already understands. A vulnerability report with a working reproducer and a candidate patch lands in a codebase the maintainer knows intimately, so the new thing is small relative to an existing mental model and cheap to check. OpenSSL’s Anton Arapov says as much in Anthropic’s post: when a report comes with a real exploit attached, “that’s basically job done for an engineer as you can verify it right away.” A long proof built on what Moshkovitz called “some alien craziness,” an entirely new recursive code, lands somewhere nobody has a model at all. The Lean certificate plays the role of the reproducer for correctness, but there’s no equivalent reproducer for understanding, which is why the same volume of output can feel like a gift to a maintainer and a tax to a mathematician.

where this argument is weakest

The strongest objection is that we already depend, constantly, on things nobody understands in full. Nobody reads compiler output. The four colour theorem was accepted on the strength of a computer check few mathematicians claim to follow line by line. Any node_modules folder is a monument to trust in strangers. If comprehension were really required for code to be valuable, modern software wouldn’t exist.

I think that’s right, and it sharpens the claim more than it kills it. We rely on compilers because their inputs are understood, their behavior is specified, and an enormous amount of comprehension went into the compiler itself, and we rely on dependencies because someone maintains them and answers for them. Unread code is fine when there’s an understood boundary around it and a responsible party behind it. Agent-written code raises the question of whether that boundary still exists, and in a PR that touches your own business logic there’s no one else’s boundary to hide behind.

There’s an asymmetry with mathematics, too. A true theorem stays true, so a community can afford to bank an unread proof and come back to it in ten years. Software rots: requirements change, dependencies drift, and someone has to modify the code next quarter with a working model of why it is the way it is. In that narrow sense software needs comprehension more urgently than mathematics does, even though our artifacts are a good deal less profound. 😅

The other serious objection is that the comprehension bottleneck may be temporary. Moshkovitz spent the following day asking an AI model to explain the UGC construction, and within roughly a day of her first texts Aaronson reported that she “now mostly understands the proof” and wants to give talks about it. That’s a remarkable turnaround, and I’d be delighted if agents became excellent explainers of their own work. But a commenter on the same thread raised a point I found unsettling, wondering how much of the clarity people perceive when they press a model for explanations “is just their own informational contribution reflected back at them.” An explanation helps you comprehend, but it can’t comprehend on your behalf, and it doesn’t move the responsibility anywhere.

norms worth borrowing

What I find genuinely useful in the math community’s response is that it’s trying to write the norms down, which software mostly hasn’t. The advisory group asks producers to have “the model, or some other model” write each proof readably, to disclose prompts, compute and how often the model failed, to state each result’s formalization status, and to pay for the understanding they haven’t supplied. Translated into engineering, that gives me three questions any team merging agent PRs should answer for itself. My answers are proposals worth trying, not settled practice.

What evidence should come with an agent’s PR? Making a change reviewable should count as part of the agent’s job, so I’d want:

  • The intent in the reviewer’s terms: the problem, the linked issue, which interfaces and callers the change touches, and what the agent chose not to do and why.
  • A ledger of checks: what was machine-checked (tests, types, invariants, an independent verifier), against which revision, and just as explicitly what wasn’t, so “the tests pass” can’t quietly stand in for “this is right.”
  • A reproducer where one makes sense, a test that fails before the change and passes after, which connects it to the reviewer’s existing mental model the way a working exploit does for a vulnerability report.
  • The dead ends: approaches abandoned and roughly how many attempts it took.
  • A named human who has read all of that and can answer why.

Who needs to understand the change, and how deeply? Not everyone, and not always all the way down. The compiler objection suggests the line: code behind an understood boundary with a responsible party can be trusted at the boundary, and code inside your own business logic can’t. So I’d try two depths. Every reviewer needs boundary depth, meaning what the change does, which invariants it relies on, and what the checks cover and leave out. Anything headed for the core of the system also needs one person at modification depth, able to change it next quarter without the agent, explain it to a teammate without opening the transcript, and predict roughly how it will fail. A generated API client probably needs only the first and payment logic needs both, and I’d rather a team decide which is which ahead of time than during an incident.

How should a team measure what review and maintenance cost? Rather than PRs opened, I’d look at reviewer hours per resolved issue, and break time-to-merge down by change size and by each reviewer’s open load, which is the only way I can see to separate the Jellyfish explanations in your own repo. If review slows even for small changes on lightly loaded reviewers, comprehension becomes a much more plausible culprit. For maintenance I’d watch how often agent-written code is reverted or reworked within a few weeks, how long its first human modification takes compared with similar human-written code, and how many people have reviewed or changed each module, a crude bus factor for understanding. Like the patched count, none of these measures comprehension directly, and the dashboard should say so. They measure the cost of not having it, and when agent output keeps outrunning a team’s capacity to understand it, I think the honest response is to slow the output rather than thin the review.

the slow part

I still want the agents to cook, and I still want them to prove it. What this week changed is the order in which I hold those two ideas. The last post was about earning enough trust to let an agent work alone, and this one is about what that trust doesn’t buy, which is someone who can answer for the code in six months when something odd happens in production.

The image I keep returning to is Moshkovitz, a day after receiving a proof of the conjecture she’d worked toward for so long, asking questions until the alien construction became something she could explain to a room full of colleagues. The machine did the fast part. The slow part, turning a certified result into something other people can build on, was hers, and I’d like the code my team puts in front of users to keep going through that same slow part, however good the checks get.

A passing check tells me a change is worth the effort of understanding. It doesn’t do the understanding.

things worth reading

← all posts