The problem
The absolute Galois group of a field gathers all of its Galois theory into a single object: its closed subgroups correspond to the field's algebraic extensions, so a concrete description of the group is a concrete description of every extension at once. For the p-adic numbers ℚp — the local fields sitting inside the rationals at each prime — this group has been understood by explicit generators and relations since the early 1980s, when Jannsen and Wingberg, building on the work of Demushkin, Serre, and Labute on its maximal pro-p quotient, gave a presentation of the full group for every odd prime. The prime 2 resisted: Zel’venskiĭ described the Galois group of the maximal 2-extension for 2-adic base fields of odd degree, and Diekert obtained structure results for dyadic fields under additional hypotheses, but no presentation of the absolute Galois group of ℚ2 itself was known.
The missing dyadic case was recently posed as one of Epoch AI's FrontierMath open problems. This paper closes it: the absolute Galois group of ℚ2 is generated by four elements subject to two explicit relations. Beyond completing the local story, such presentations matter because the local groups are the computable building blocks of the global one — every prime contributes a copy inside the absolute Galois group of ℚ — and an explicit presentation turns questions about extensions, their counts, and their symmetries into finite computations.
The solution
The route to the presentation ran through AI collaboration, with humans and machines checking each other at every step. A series of candidate relations, proposed in extended conversations with AI reasoning models, fell to computational tests or to review — one promising candidate was abandoned when it proved incompatible with a marking that pins down how generators map to the unramified quotient, and the repair of that failure produced the relation that survived. The final candidate was corroborated by computations over thousands of finite groups and accepted by Epoch AI's independent verifier.
Review then hardened the proof itself: two arguments in early drafts were found to be flawed and were replaced, leaving the presentation untouched. As the last step, the theorem was formalized in Lean in two separate projects, so that a machine has checked every deduction and reports exactly which published results are taken as inputs. The full source-checked story — the candidates, the failures and repairs, and the role each AI system played — is coming in the development record.