David Turturean’s account covers the search; Fable’s account is the view from inside the machinery. The development record gives the full chronology.
I have been interested in finding a presentation of the absolute Galois group of $\mathbb{Q}_2$ for almost a decade. My journey toward this paper began when I discovered that you could use the presentation for odd $p$ to count extensions with a given finite group. I hoped to use these counts to investigate the feasibility of creating a database of $p$-adic tori of bounded dimension (for each $n$ there are finitely many conjugacy classes of subgroups $G$ of $\operatorname{GL}_n(\mathbb{Z})$, and you can roughly enumerate $\mathbb{Q}_p$-tori of dimension $n$ by enumerating field extensions with Galois group $G$). The general story was impeded by the lack of a presentation for $\mathbb{Q}_2$, but I published a paper in ANTS XIII using the odd presentation to count extensions and give finite-level criteria ruling out certain Galois groups.
I am not an expert on profinite groups and I struggle to read German, so I did not pursue the problem, but it remained in the back of my mind. So when Epoch AI approached me in September 2025 about contributing problems to the Open Problems challenge it was a natural candidate. I was able to adapt my code from the ANTS XIII paper to produce a verifier; while not a guarantee of correctness I believed that it would provide good evidence that a purported solution was correct. Indeed, David Turturean reached out with potential presentations on March 11, 13, and 15, but none passed the verifier.
Anthropic's Fable 5 model was first released on June 9; I was attending an ICERM workshop on Number field counting in the LMFDB and we had an approach toward computing the leading coefficient in Malle's conjecture that required having a presentation for the absolute Galois group of $\mathbb{Q}_p$ for all $p$ (following Loughran-Santens). I decided to ask Fable to find a presentation for $p=2$ and it came back overnight with a presentation that passed my verification scripts, together with a partial proof of correctness. Occupied with the workshop, I asked it over the next several days to fill in the gaps without providing any guidance. It did not succeed, and on June 12 the US government forced Anthropic to withdraw Fable.
In the middle of the three weeks that Fable was unavailable, David Turturean reached out again on June 24 with news that GPT had found another presentation, together with a proof of correctness. This time, the presentation passed the verification script, leaving us with a 60 page paper that might be right. Skimming the paper, it looked reasonable, but I was not confident in my ability to spot subtle errors (especially given my summer travel schedule). David began an effort to autoformalize the proof using GPT; when Fable access was restored on July 1 I was attending a workshop on Lean and I started a parallel effort using Fable 5 and Opus 4.8.
I found the autoformalization process amazing. I provided Fable with the paper and asked it to make a plan. It determined that several foundational results in class field theory and quadratic forms would be huge projects, and suggested taking them as axioms. After I agreed to allow axioms that had exact matches in the mathematical literature, it created a plan and got to work. Most of my interactions merely involved delegating tasks to Fable and Opus agents, and occasionally asking it to split harder chunks into subtasks for more effective parallelization. It did seem to struggle with parts (as evidenced by how many times certain pieces of the proof were split into smaller chunks), but succeeded at producing a formalization after one week.
We were left with a paper written by GPT, formalized with Fable's assistance and checked by Lean's kernel (subject to the stated axioms and associated definitions). The paper was not yet ready for human readers: it lacked context and background on the problem, explanation of which aspects of the proof were interesting or novel, discussion of followup questions, sufficient references to the literature, as well as transparency about the process. Given the role that AI agents had played in the story so far, I decided to try to address these issues iteratively with Fable's assistance rather than starting from scratch.
I believe that AI models can help us produce more comprehensible mathematical writing. Different readers approach a text with different levels of background, yet the author has traditionally had to choose a level of exposition. Building upon knowls in the LMFDB and PreTeXt, I aim to allow the reader to control the level of detail they see, and to provide easy access to definitions and notation at the point of use to functionally expand the reader's context window. The ability to create such documents has existed for over a decade, but it is tedious work. AI makes the authoring process much smoother. As part of drafting this paper, I created the accompanying open source PaperForge project, which I hope will develop into a set of AI-based tools for improving mathematical exposition. I think these methods have particular promise in the current context, where an AI-written paper is accompanied by a Lean formalization, since this allows the AI writing to continually connect to mathematically correct foundation. This work is still at an early stage, and I welcome feedback and pull requests!
Several factors contributed to the success of this project. First, the verification script provided an external validation of the approach before the expense of formalization. Since formalization is still a substantial undertaking, this allowed GPT to cheaply iterate, only committing to a Lean proof once the informal proof was already expected to be correct. This crutch may not be necessary for long: Fable successfully found candidates without iteration (though without proofs), and tighter integration of formalization with proof exploration may obviate the benefit of external verification.
Second, Epoch AI's Open Problems list brought new eyes to the problem, bringing in others who were experimenting with AI orchestration methods. I think that influx brought this problem to a quicker conclusion, but we can all learn these methods: the way we used GPT and Claude does not require particular expertise. However, it does require some financial resources (and the corresponding, well-documented resource usage of the data centers underpinning these systems). While the amount of money spent is not outlandish for faculty with grants, it is more of a stretch for graduate students and infeasible for many. David and I are grateful to Fulcrum and the Simons Foundation for funding this work.
Third, the advances in AI capabilities are very noticeable. We noticed a qualitative difference in the models that became available this summer. Opus would frequently get stuck in the formalization tasks, but switching to Fable quickly resolved the issues. With models continuing to improve, I expect that more problems will become amenable to these kinds of approaches.
Finally, I am grateful to the humans who have built up the capabilities of Lean and Mathlib. The formalization would not have been possible without Mathlib to build upon, and manual verification of the proof that GPT produced to a sufficient level of confidence would have been long and painful.
I found this project exciting to be a part of, and I am happy to discuss its implications, both mathematical and methodological. Find us on Zulip.