The Morgan-Mullen conjecture states that every finite field extension 
contains a completely
normal element that also generates the multiplicative
group of 
(Morgan and Mullen 1996). Complete normality means that the same element generates
a normal basis over every intermediate field,
rather than only over 
.
Hellwig (2026) reports a proof for every prime power 
and 
.
The accompanying Lean formalization covers the new 
argument but assumes the previously known 
theorem and a Rosser-Schoenfeld bound as axioms. The
large computations additionally trust Lean's compiler and interpreter. These declared
inputs and computations require verification beyond the formal kernel check, so the
reported general resolution retains those qualifications. Hellwig (2026) states that
AI generated the mathematical arguments and the formalization under the author's
direction, and that the author checked the final proof
by hand.
