mirror of
https://github.com/merlinhu1/Battle-tested-Research-Prompts.git
synced 2026-08-26 12:20:55 +02:00
A Presentation of the Absolute Galois Group of Q₂
| Field | Number theory |
|---|---|
| Researcher | David Roe / David Turturean |
| Model | GPT-5.5 Pro |
| Date | Jun 24, 2026; manuscript and formalization record Jul 26, 2026 |
| Status | Very strong; public FrontierMath prompt, detailed development record, and two Lean formalizations |
| Prompt | prompt.md |
Result
The prompt asks for an explicit profinite presentation of the absolute Galois group of the 2-adic numbers. The public record reports an explicit presentation with four generators and two relations, followed by independent Lean formalizations and finite-quotient verification.
Provenance and verification
- FrontierMath problem and exact prompt
- Roe's development and success record
- Paper and presentation
- Reproducibility instructions and verification limits
- Roe's Lean formalization
- Turturean's Lean formalization
The Lean checks are kernel-checked subject to their stated axioms. The finite quotient verifier is strong supporting evidence, not by itself a proof of all finite quotients.
Prompt techniques
The prompt fixes a strict output grammar, supplies useful pro-2 background, and gives an analogous p=3 presentation. This makes the task machine-checkable while leaving the central construction open.