Almost all primes are partially regular

Source: arxiv:2602.05090 Authors: Evan Chen, Kenny Lau, Seewoo Lee, Ken Ono, Jujian Zhang Status: verified Main declarations: LeanPool.PartialRegularity.Extension.irregularPrimes_isBigO Tags: number-theory, asymptotics MSC: 11B68, 11N05

Mathematical overview

Let ℕ = {0,1,2,…} and let B_{2k} ∈ ℚ be the (2k)-th Bernoulli number. For m ∈ ℕ a prime p is m-regular if p is odd and p does not divide the numerator of B_{2k} for every k with 1 ≤ 2k ≤ min(m, p - 3). Fix a real α > 1/2 and set M_α(p) := ⌊√p / (log p)^α⌋. The main result irregularPrimes_isBigO shows that, as X → +∞,

#{ p ≤ X prime : p is not M_α(p)-regular } = O(X / (log X)^(2α)),

with explicit constant 10 for every α > 1/2.

Provenance

Imported from https://github.com/AxiomMath/partial-regularity; the upstream Lean files were generated by Axiom Math and accompany the paper arXiv:2602.05090. Upstream is MIT-licensed and contains no sorrys in the imported extension file. Ported from Lean v4.26.0 to Lean Pool's v4.30.0-rc2.