Explicit Presentation of the 2-adic Absolute Galois Group
Statement
Give an explicit profinite presentation of . The tame local cases were settled by the early 1980s; the dyadic case was the last one missing. The new presentation has four generators, two word relations and a pro- condition on the wild generators.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
construction · #1
ChatGPT-5.5 Pro (GPT-5.6 A, B), Claude Fable 5, Claude Opus 4.8, with David Roe and David TurtureanThe record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.
A ChatGPT Pro conversation produced the candidate presentation with an informal proof; it passed Roe's finite-quotient verifier on all 5,402 test groups, and the proof was then formalized twice in Lean 4 with coding agents.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
Two separately initiated Lean 4 formalizations, checked modulo 7 and 9 named interfaces to the classical literature respectively. Manuscript public with an interactive web edition; not yet externally peer-reviewed.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.