Direct discovery · Mathematics

AxiomProver formalizes components of new proofs of Thakur’s power-sum hypotheses

Proofs of H1 and H2 over prime fields and H3 over arbitrary finite fields, with conditional Lean formalizations of their components.

Summary

Chen and Ono prove cases of three hypotheses posed in 2009 about finite-field polynomial power sums. AxiomProver supplies formal components, while the paper explicitly leaves the bridge relying on Sheats’ theorem outside the formalization.

AI role

Translated author-supplied arguments into Lean across separate H1, H2, H3 and auxiliary-lemma tasks.

Narrative role

Documents AI-assisted checking of new research mathematics and makes the boundary between formal components and the whole argument explicit.

Caveat

This is AI-assisted formalization, not evidence of autonomous theorem discovery. H1 and H2 are limited to prime fields; the formal development assumes an unformalized bridge. No independent Lean build was performed in this run.