Doing small AI-assisted math and recording every step

On September 8, OpenAI announced that a swarm of roughly ten thousand coordinating agents, running an unreleased model for 88 hours, had produced a solution to Navier-Stokes, one of the Millennium Prize problems (famous unsolved problems, each with a million-dollar prize). OpenAI said the proof was verified in Lean, a programming language for proofs: if a Lean file compiles cleanly, a computer has checked every step, but only of the statement as written in Lean. The news reports did not say that anyone outside OpenAI had checked it. Terence Tao's reaction, to CNN: "It's a little like going to watch a movie and jumping straight from the first ten minutes to the last ten minutes; technically, all the plot lines are resolved, but most of the value of the experience was lost." Then the line that stuck with me: "the indiscriminate use of AI is turning the subject into a meaningless production quota 'game' that ultimately is of very little benefit, either to mathematics or to the world." There is also a dispute over who deserves credit. The news entry on this site covers it, with sources.

I cannot judge whether the proof is right, because I can't read it, and very few people can. What I can offer is my records from doing much smaller AI-assisted math, and I think they are useful to read next to the headline.

The work itself is small and checkable on purpose. When I wrote this I had thirty-four contributions credited to me in the OEIS, the reference database mathematicians use to look up number sequences (43 as of October 20, 2026), each one checkable by its A-number, the catalog number the database gives every sequence. In July I extended the published records for twelve unsolved games from combinatorial game theory, on one machine; Achim Flammenkamp, who maintains the tables the field cites, reran two of the games on his own computers with his own code, got the same answers, and listed the work under my name. And I found and fixed a digit that had been missing from a published sequence for fourteen years, after recomputing the correct value with a second, independent program to confirm my first answer.

I keep a record of everything I do with AI in my research: one line, written the same day, for every result, decision and failed attempt, and every paper sent out. I never edit a line; a correction goes in as a new line. From that record I wrote a set of standards. Each standard came from an error that one of my checks had found, and I keep a separate file of those errors.

On September 12 I gave the same set of checks a different kind of question: did a public dataset of 25.8 million Los Angeles parking tickets hold a new, publishable paper? One AI agent led and eleven helper agents each took one job. One helper's whole brief began "KILL a research idea by finding prior work that already does it." The agents worked for about an hour in all, split by a pause of about 22 hours, and just over twenty-three hours after the first instructions the answer was not yet: on the five-point scale the project set for itself, where 3 was the bar to start writing, the idea scored 2. I recorded that result in the same detail as the successes.

This is where my records connect to Tao's complaint. If nobody can read a proof or inspect the process that produced it, nobody can repeat the work. A mathematical result is more useful when it comes with a record of what was tried, what failed, what each check tested, and who else confirmed it. When I use AI agents on a problem, I have them keep that record, and the record is what I would defend.

My results are much smaller than a Millennium Prize: the record, a few dozen OEIS entries, a records page with my name on it, and a dropped idea written up as carefully as the ones that worked. Whatever happens with AI math at large scale, I can show every step of this work.

Drafted with Claude, like everything here, and checked against my research record before it went up.