Post #4360749

2026-08-03 15:17 UTC

The '2-adics' are numbers in base 2 that can go on infinitely in both directions, like this: ....0101001111010.0000101011110101.... You can add, multiply, subtract and divide them, so we say they form a 'field'. We call the field of 2-adics ℚ₂. Last week, humanity solved a huge problem about ℚ₂. The problem was to figure out the so-called 'absolute Galois group' of ℚ₂. I'll explain what that means, but first I want to say: we can cook up a field of p-adics for any prime p, and this problem had been solved for all p-adics except the 2-adics! Oddly, the smallest prime is even harder than the rest! Here's the rough idea. Starting from any field, you can cook up a larger field that contains the solutions of all polynomial equations whose coefficients are in your original field. This is called the 'algebraic closure' of your original field. For example, the algebraic closure of the real numbers is the complex numbers, since there are lots of polynomial equations like x²=−1 that don't have real solutions - but they all have complex solutions. The complex numbers have an interesting symmetry called 'complex conjugation', sometimes written with a *. I say it's a symmetry because (x + y)* = x* + y* (xy)* = x* y* and so on for subtraction and division. Of course, complex conjugation has no effect on real numbers: if x is real, we have x* = x. This idea is interesting to generalize! Given any field F, its algebraic closure will have a bunch of symmetries that have no effect on elements of F. These symmetries are called the 'absolute Galois group' of F. So what is the absolute Galois group of ℚ₂? David Roe and David Turturean figured it out. (1/n) https://roed314.github.io/gq2/

Replies (1)

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

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)

Open ##4360865