Almost All Primes are Partially Regular
Statement
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.
Record
- Source
- Added
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
AxiomProver, with Evan Chen, Letong Hong, Kenny Lau, Seewoo Lee, Ken Ono, Jujian Zhang and and the AxiomProver engineering teamThe record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.
"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.
Machine-checked by Lean on #1 · not a person
lean: partially checkedLeanscope Lean formalization of the core argument; statement correspondence not independently audited
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.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.