Almost All Primes are Partially Regular
In the circle of Kummer's regular primes and Vandiver's conjecture, the paper proves that almost all primes are partially regular, yielding a partial Vandiver theorem for a density-one set of primes, with consequences for Kubota-Leopoldt p-adic L-functions, Eisenstein congruences and K-theory torsion.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Algebraic number theory
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-02-04
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- Evan Chen, Letong Hong, Kenny Lau, Seewoo Lee, Ken Ono, Jujian Zhang, and the AxiomProver engineering team
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
"The theorem proving partial regularity for almost all primes is fully formalized in Lean/Mathlib and was produced automatically by AxiomProver from a natural-language statement of the conjecture." The human authors prepared the mathematical exposition from the formal development as reference.
Verification
Fully formalized and kernel-checked in Lean/Mathlib, produced autonomously by AxiomProver; no independent review of the informal-to-formal correspondence yet. Tier: AxiomProver produced both the proof and the Lean statement; the correspondence to the informal claim has not been independently audited.