Prime-factor statistics of p − 1
Prime-factor statistics of p − 1 is a family of three manuscripts dated September 2026 in OpenAI's public mathematics collection (github.com/openai/math). They concern the prime factors of the predecessor p − 1 of a prime p, and one of them addresses Erdős's conjecture on the largest fibres of Euler's totient function (Erdős Problem #821). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Totient fibres and smooth shifted primes. For every ε > 0, infinitely many positive integers n have more than n1−ε solutions m of φ(m) = n. The arithmetic input is that, for every fixed 0 < δ < 1/4, at least x1−o(1) primes p with 2x < p ≤ 5x have every prime factor of p − 1 at most xδ; the manuscript notes that the count also holds for every fixed δ > 0. Source: Weighted dilation graphs, smooth shifted primes and totient fibers (24 September 2026).
- Poisson–Dirichlet law. For a prime p chosen uniformly from 3 ≤ p ≤ x, the logarithms of the prime factors of p − 1 (in decreasing order, with multiplicity), divided by log(p − 1), converge in every finite joint distribution to the Poisson–Dirichlet distribution with parameter one. The manuscript states that this proves a conjecture of Ford, Konyagin and Luca. Source: The Poisson-Dirichlet law for prime predecessors (24 September 2026).
- Even number of prime factors. There are infinitely many primes p for which p − 1 is squarefree with an even number of prime factors, that is, μ(p − 1) = 1. Source: Prime predecessors with an even number of prime factors (17 September 2026).
- Formalization. The collection's index (commit
adc7f12) lists no Lean formalization for this family. - Earlier results, as summarized in the totient-fibre manuscript. Pomerance (1980) formulated the conjecture as C = 1, where C is the supremum of exponents c with g(n) > nc infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
- Problem database. The erdosproblems.com entry for Problem 821 (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | J. Guo, aster2024/openai-math-followups (GitHub), consequences list, item 2 | Use (conditional consequence) | Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (x5/12−ε, and x0.4736−ε with Harman's admissible value) and for Novak–Carmichael numbers (x1−o(1)). | The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content. |
| 2026-10-11 | S. Li, Z. Zhuang, Coprime pairs with equal sum of divisors, assuming smooth shifted primes (arXiv:2610.15674, v1; Lean code at daizisheng/erdos-824, Palomar PALOMAR-2026-10-11-000021, version 1) | Use (conditional) | Erdős Problem 824: the number of coprime pairs a < b < x with σ(a) = σ(b) is x2−o(1), conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of p − 1 the authors check transfers to p + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. | arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates. |
| 2026-10-14 | Yao Xu, cadamcat/totient-fibers-lean4 (GitHub; commit dfce357) |
Formalization (Lean) | A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. | Author-reported; the README states that the work was developed with AI assistance. |
| 2026-10-14 | Yao Xu, cadamcat/equal-divisor-sums-lean4 (GitHub; commit 6280393) |
Formalization (Lean) | A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs a < b < x with σ(a) = σ(b) exceeds x2−ε for all large x, with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes p = 2u − 1 with p + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. | Author-reported; the README states that the work was developed with AI assistance. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.