Post #4360865

2026-08-03 15:43 UTC

I know how much most of you hate AI, so you'll be disgusted to know that this one was proved with a huge amount of help from various LLMs. But I'm really interested in the future of mathematics, and this is a theorem that actually seems very significant to me. So I had to read the accounts provided by David Turturean: https://roed314.github.io/gq2/development/account/ and David Roe: https://roed314.github.io/gq2/development/success/ and Claude Fable 5: https://roed314.github.io/gq2/development/fable/ I think this material is quite good for explaining how the result was found and later formalized (twice!) in Lean. They provide an estimate of the cost of the project: https://roed314.github.io/gq2/development/cost/ They also provide an interactive paper: https://roed314.github.io/gq2/paper/paper.html where you can choose the amount of detail you want to see. Unfortunately the paper is extremely technical, and it lacks the kind of basic survey of what's going on that would help a nonexpert like me understand the broad outlines! There's no way I can tell for sure if this stuff is for real. Since I've never tried to understand the absolute Galois groups for p-adics with p ≠ 2, jumping into the 2-adic case is like practicing mountain climbing by going straight for Everest. (Actually the real Everest is the rational numbers: nobody yet has figured out its absolute Galois group.) But if I had to guess based just on my mathematical gut feel, I'd guess this stuff is real. Anyway, let me quote Turturean, since he explains the strange way this theorem was proved. (2/n)

Replies (1)

@johncarlosbaez@mathstodon.xyz 2026-08-03 15:50

David Turturean writes: "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?" However, if you read the whole story you'll see it required a lot of work, and an expert in solving math problems using LLMs (David Turturean), and a real expert in Galois theory (David Roe), to bring the research to this point. (3/n, n = 3)

Open ##4360864