David Roe’s account covers verification, formalization, and writing. The development record gives the full chronology.
By early 2026, it had become clear that AI was poised to solve a lot of open problem in mathematics.
AI was starting to eat away at the Erdős Problems list by solving some of them with just one prompt. AI was also now able to do cognitive labor that would take a human a workday (so a few hours) in other fields. In January of 2026, I thought to myself: why not make AI work for many workdays in a row towards a certain problem, the way a research mathematician would? If each time you prompt an AI model, it outputs the technical volume that a human mathematician could produce in about a day, why not repeat that and hope it generates what a human mathematician produces in a week, month, or year?
Throughout January and February, I played around with deploying this idea. I eventually landed on a harness on top of ChatGPT-Pro that prompts the model with its own history of attempts to continue solving a given problem. You can see the details of this in the logs. One thing I found important is that, each time I prompted ChatGPT to attempt an open problem, I should start a new conversation thread: through their post-training, LLMs are made to not derail a conversation, meaning that an LLM will only be so exploratory, self-critical and innovative once you have a few back-and-forths with it in the same ChatGPT conversation. This could have changed in the meantime, since LLMs are generally now more eager to take open math problems, but at the time I found a huge difference in progress if I kept the research prompts all within the same conversation vs. if I initiated a conversation each time I inquired furthermore.
Instead of coding up this harness that would let me prompt GPT-Pro autonomously ad infinitum, I let Claude Code code it up: I did not want to have to type a command each time I wanted to run certain routines, but rather I wanted to be able to tell Claude Code in natural language to run or edit the routines. So instead of me forcing a shape of the approach onto Claude Code, I let Claude Code auto-discover what is the best way to do that for itself.
I next turned to the FrontierMath Open Problems set, first chipping away at explicit deformations and Ramsey book graphs, then sending David Roe promising candidate presentations for the 2-adic Absolute Galois Group. Unfortunately, none of the three ones I had sent before June 2026, found and elaborated by ChatGPT-5.2-Pro and ChatGPT-5.4-Pro, passed David Roe's computation verifier. Motivated by the nonlinear connections LLMs pick up on in math through their training, I had tried to get the models to first guess a promising candidate, then prove the correctness of said candidate: the models could neither prove nor disprove a lot of the promising candidate presentations they had found. I also tried to get the models to start from a promising general shape of a proof of correctness that a candidate would have, without a specific promising candidate in mind - and then try to 'fill in the blanks' of the proof with said candidate: that also did not work.
Eventually, according to X (formerly known as Twitter), GPT-5.6-Pro was in stealth deployment, or A/B testing, and, indeed, when I tried to use "GPT-5.5-Pro" in the second half of June through the web portal, it was significantly better and thought for longer. So I attempted this problem again.
During a ~26-hour autonomous stretch, Pro found a candidate called A2 and developed a substantial proof around it. It worked out calculations over finite target groups, organized inductions intended to cover a lot of interactions between it and other groups, and generated a journal-style manuscript. At this point, I had also asked separately GPT-5.6-Pro to develop a number of tests of varying oddity and complexity to verify the candidate: every case my local package could handle agreed with A2.
I opened a separate ChatGPT Pro review of the A2 manuscript. It found that a Lemma 3.4 in this manuscript motivating the correctness of A2 was false. A few turns of ChatGPT-Pro doing analysis located the defect in the candidate itself: A2 was incompatible with data that the known Galois group requires.
My next instruction was to find a more general candidate that preserved the usable part of the proof while making the missing step possible. Pro immediately derived a corrected relation, tantamount to a generalization of the initial A2 candidate, and proposed the presentation proved here, whose corrected wild relation is $h_0u_1^{-1}x_1^{\sigma}c_0=1$. We have since verified it, and it motivated the existence of this website.
Much of this work done to solve this problem was done by voice. With
a lot of the infrastructure already in place from solving other open
problems, I used Claude Code as the operational controller and most
often gave it procedural instructions by voice. This was partly
motivated by the fact that I was trying to solve a lot of problems in
parallel, partly motivated by the
fact that voice simply allows for more natural intention expressivity,
which coding agents can now pick up on. I also used speech-to-text in
the ChatGPT conversations while developing the manuscript.
This was my first sustained attempt to direct a mathematical research
process primarily through speech. This entire experience has made me
question what true effort in mathematics will look like in the future,
now that you can elicit solutions to decades-old research questions in
mathematics with your voice: can you one-shot entire PhD theses by just
talking about them, thinking about them? This is also exactly the kind
of thing that you predict becomes possible a few tens of months before
you can make things float with just your voice.
After I produced the preserved 60-page manuscript that motivated the presentation we have today, I sent the solution over to David Roe, who ran the finite-group verifier he had built for EpochAI.
After submission passed every one of his tests, he also read the manuscript and confirmed the natural-language proof.
Roe and I separately formalized the solution with coding agents. His official logs record Fable 5 and Opus 4.8, with Fable 5 used most often. I used GPT-5.5 in Codex and ChatGPT-5.5-Pro, followed by Fable 5 and some Opus 4.8 work once Fable became available again. To start, I asked GPT-5.5-Pro for a rough autoformalization plan based on the manuscript, then let GPT-5.5 in Codex query ChatGPT-5.5-Pro in-browser for incremental new formalization patches of Lean 4 code, and had Codex integrate and compile each new piece of Lean code from Pro. The development record includes the formalization records, and the cost page the machine-readable token audit.
Once Fable became available again, I used it for the last details. I had seen people on X describe it as state of the art, and in practice it repeatedly produced 700-plus-line patches of Lean in a single response, many times in succession. Roe had never attempted an autoformalization before, yet his Fable-led effort produced a separate development containing roughly 90,000 tracked lines of Lean source within about two weeks. This came immediately after my Erdős Problem #870 formalization, which, as far as I could find at the end of June, was the largest one-person autoformalization of a single problem. The compression in required experience and elapsed time points toward a future where “you can just formalize things.”
After Roe's autoformalization finished, I completed my development with a patch from his separately developed formalization; this patch represents 3-4% of my formalization, however was very helpful as models can get slow and lazy towards the last-mile delivery of an autoformalization.
Fulcrum provided the great majority of the compute I used throughout the successful solution search and my Lean formalization.
Roe created PaperForge and assembled the PDF, interactive paper, formalizations, and development record into the site where this account appears. He has been immensely helpful in corroborating the artifacts that a mathematician would find necessary to digest an AI-generated result.