An explicit presentation of the absolute Galois group of ℚ₂

AI models produced a candidate explicit presentation of the absolute Galois group of the 2-adic numbers, the one case left open; Lean formalizations exist but rely on cited results, and the write-up is not peer reviewed.

Problem
Give an explicit presentation, by generators and relations, of the absolute Galois group of Q2\mathbb{Q}_2.
Credit
Claude Fable 5 (per Epoch AI) and GPT-5.5 Pro, with David Roe and David Turturean · Human-elicited AI solutions
Checked
Two Lean formalizations relying on cited resultsMarked solved by Epoch AI
Timeline
Claude Fable 5 solution 2026-06-09 → GPT-5.5 Pro solution 2026-06-24 → write-up 2026-07-26
Sources
Epoch AI problem pageWrite-up by Roe and Turturean
UN-
VERIFIEDLean with external inputs · not peer reviewed

The problem

The absolute Galois group of a field encodes all of its finite extensions at once. For the pp-adic numbers Qp\mathbb{Q}_p with p>2p > 2 explicit presentations by generators and relations are known; the case p=2p = 2 was open.

What AI did

According to Epoch AI, the problem was first solved by Claude Fable 5 in a session run by David Roe on 9 June 2026, and David Turturean obtained a solution with GPT-5.5 Pro on 24 June. The write-up by Roe and Turturean (26 July 2026) gives a different account: it says a ChatGPT Pro session found the candidate presentation and an informal proof.

How it was checked

There are two Lean 4 formalizations; one relies on 9 cited results from the literature as interfaces, the other on 7 external inputs. Epoch AI's verifier matched the predicted number of extensions for 5,402 test groups, which Epoch calls strong evidence but not a proof.

Limitations

The write-up is not peer reviewed and has no archival identifier, the formal proofs depend on results taken from the literature, and the sources disagree about which model found the presentation. We grade it "unverified" for now. Problem description paraphrased from Epoch AI (CC BY 4.0).

∎