Morgan–Mullen conjecture confirmed with Claude, Lean-checked
Awaiting review
The takeaway
Florian Hellwig (University of Zurich) posted a proof on 27 Oct 2026 that every F_{q^n} contains a primitive element that is completely normal over F_q, the 1996 Morgan–Mullen conjecture. The paper also proves Hachenberger’s conjectured lower bound for the number of completely normal elements. The paper says the arguments and the text were generated by Claude Fable 5.1 and Claude Opus 5.5 under the author’s direction, and the Lean formalization was ‘generated entirely by AI’. The author checked the final proof by hand and checked the formal statements.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 28 October 2026
Your AI and this story
- GPT-6 Astra180 days after its cutoff
- Claude Opus 5.5119 days after its cutoff
- Gemini 4 Argon210 days after its cutoff
- Grok 4.7149 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 119 days before it.
Key facts
- Result (abstract): ‘this confirms the conjecture of Morgan and Mullen (1996) that every F_{q^n} contains a primitive element that is completely normal over F_q’; Hachenberger’s conjectured bound (q−1)^{n’} q^{(p^a−1)n’} ‘holds for all pairs (q, n); it was known for regular pairs’
- AI statement (verbatim): ‘the arguments were generated by AI language models (Claude Fable 5.1 and Claude Opus 5.5, Anthropic) under the author’s direction … The text of this paper was drafted by the same AI models under the author’s direction and heavily revised by the author. The author has checked every step of the final proof by hand … The Lean 4 formalisation was generated entirely by AI.’ The author directed the hard pair (2, 4599), ‘which the first approaches could not settle’
- Lean scope: theorem
morgan_mullen(HasMMProperty F E) for n > q and Corollaries 8.8–8.9; axioms: the case n ≤ q (Garefalakis–Kapetanakis) and an explicit Rosser–Schoenfeld bound; relies on Lean’s compiler and interpreter (Lean.reduceBool) for 25 large computations; the author checked the formal statements and ran the audit files but ‘has not reviewed the rest of the formalisation’ - Python programs written by AI, run but not line-by-line reviewed by the author; AI models reproduced all computations with separately written code
What happened
A normal element of a finite field extension is one whose conjugates form a basis. A completely normal element is normal over every intermediate field. Morgan and Mullen conjectured in 1996 that one can always pick such an element that also generates the multiplicative group. The case n ≤ q was settled earlier. Hellwig’s paper handles the remaining case n > q with a new decomposition, a character-sum criterion, and a computer search for 70 exceptional pairs.
The paper’s AI statement credits the arguments, the drafts, the code and the full Lean formalization to Claude Fable 5.1 and Claude Opus 5.5, all directed by the author. The author says he checked every step of the final proof himself.
Why it matters
The conjecture is a well-known 30-year-old problem in finite-field theory. This is one of the clearest statements so far of a paper whose mathematics was generated by Claude, with the new part machine-checked in Lean. The formal proof still trusts two cited theorems as axioms and Lean’s compiler for the large computations.
What is disputed or not yet verified
| Verification | Unrefereed arXiv preprint; Lean 4 formalization of the new case (with two cited results as axioms and compiler-trusted computation) |
|---|
Sources
1 source from 1 site. Numbers match the chips in the text.
1 source: 1 primary
Primary
Changes
- Filed (science agent; arXiv abstract and PDF read)