Largest prime factors of consecutive integers
From OpenAI Aftermath
Largest prime factors of consecutive integers concerns the joint distribution of the largest prime factors P(n) and P(n + 1) of two consecutive integers: whether, in natural density, they behave like independent smooth-number statistics, and in particular whether P(n) < P(n + 1) for exactly half of all integers, a question attributed to Erdős and Turán and listed as Erdős Problem 371. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the joint Dickman law in ordinary natural density and deduces that each ordering has density 1/2. The collection includes a Lean formalization of both statements. This page summarizes the published claim 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.
Background
- As recounted in the introduction of the manuscript:
- The theory of smooth numbers of Dickman, Ramaswami and de Bruijn gives the density ρ(1/a) of integers n ≤ X with P(n) ≤ Xa, where ρ is the Dickman–de Bruijn function.
- Erdős and Pomerance formulated the joint independence problem and proved that each ordering of P(n) and P(n + 1) has positive lower density; the lower bound was raised by de la Bretèche, Pomerance and Tenenbaum, by an observation of Fouvry, by Wang, by Lü and Wang, and by Yang.
- Teräväinen proved the joint law in logarithmic density, Tao and Teräväinen obtained it for ordinary averages outside an exceptional set of scales, Wang proved it under an Elliott–Halberstam conjecture for friable integers, and Jiang, Lü and Wang established averaged-over-shift forms.
The original result
- Claim. Theorem 1.1 of The joint Dickman law for consecutive integers states that for every fixed a, b in (0, 1), the proportion of integers 2 ≤ n ≤ X with P(n) ≤ na and P(n + 1) ≤ nb tends to ρ(1/a)ρ(1/b), with ordinary counting and the limit over all real X. Corollary 1.2 states that P(n) < P(n + 1) holds on a set of natural density 1/2, and so does the reverse ordering. The manuscript states that the fixed-threshold form of the theorem also gives the upper-tail independence conjecture of Erdős and Pomerance.
- Method, as described: a mixed decorrelation statement for labels attached to the bins of the largest prime factor is proved by contradiction, using a profinite profile, a divisor amplifier, a graph on rough divisors, a comparison with a finite-rank kernel and short-interval cancellation in the style of Matomäki, Radziwiłł and Tao.
- Sources. The manuscript The joint Dickman law for consecutive integers at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the joint Dickman law in ordinary natural density for every 0 < a, b < 1, and that each of the orderings P(n) < P(n + 1) and P(n + 1) < P(n) has natural density 1/2. The Comparator statement is
JointDickman.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the headline law and the corollary on the orderings are stated. It notes that the Dickman function is a custom construction through its delay equation, which it describes as correct by inspection, without a bridge lemma to a Mathlib object. It records no Comparator run for this challenge. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 (latest commit 10 October 2026) | jbaelaw/Erdos928 (GitHub, commit 68fe47b) |
Use (Lean) | A Lean formalization, using Mathlib only, of an explicit counting bound and a transfer of natural density between the strict and non-strict threshold conditions, from which the joint Dickman law of Theorem 1.1 gives the strict, shifted-threshold formulation of Erdős Problem 928. The README states that the repository does not re-prove or import OpenAI's analytic theorem and claims no independent solution of the analytic problem. | The README reports a passing build with the standard axioms and a Comparator run in its paranoid mode. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the JointDickman solution, in 2,715 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list JointDickman, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-11 | Google DeepMind Formal Conjectures, Erdős Problem 371 (commit 3dfd999, pull request #6898) |
Catalogue (formal statement status) | States Erdős Problem 371, that the integers n with P(n + 1) > P(n) have density 1/2, marks it as solved, cites the manuscript, and links the collection's Lean proof as its formal proof. | Merged into the repository. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap, with one minor note that it describes as a warning rather than a located failure. The steps it read use only that the labels have modulus one, invariance under fixed small multipliers and short-interval cancellation, so the same argument appears to apply to the Liouville function and would give binary Chowla in ordinary density, which it describes as still open; the paper does not discuss this. It names the comparison of integrals in the kernel and channels sections, which it did not verify, as the likeliest weak point if the argument does transfer, and states that it could not identify a failing inequality. It also lists the arithmetic, moments, channels and distribution sections and part of the kernel section as not verified. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. The collection separately claims the two-point Chowla conjecture; see The two-point Chowla conjecture. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
