Erdős Problem #371

Read our full write-up →

Write P(n) for the largest prime factor of n. Erdős and Pomerance stated in 1978 (the question goes back to Erdős and Turán) that P(n) < P(n+1) should hold for exactly half of all n, in natural density, and more: that the sizes of P(n) and P(n+1), measured as powers of n, are independent, each following Dickman's law. Teräväinen proved this in logarithmic density in 2018, Tao and Teräväinen at almost all scales, Wang under the Elliott–Halberstam conjecture for smooth numbers; the best unconditional lower bound for the ordering was about 0.3. OpenAI's preprint of 24 September (84 pages, public since 6 October) proves the full joint law in ordinary natural density, so both orderings have density exactly ½. Its Lean proof — a 1,836-module closure, with patched copies of two prime-number-theorem libraries — was kernel-replayed on our machine, and its statement matched the paper. Four hostile AI seats read the paper and the Lean: HOLDS AS READ. The formal proof does not use the Matomäki–Radziwiłł theorems the paper cites. What is ours: the replay, the readings, a Lean proof of Formal Conjectures' erdos_371 from OpenAI's library (FC marked it solved on 11 October, but its proof is still sorry, and the merge commit's reviewer notes list the density-convention step as missing), an unconditional Lean proof of #928 as Erdős posed it (strict inequalities, threshold (n+1)^β; a third party had formalized the implication from the joint law, as a hypothesis, on 9–10 October), the observation that Erdős's other question in #371 — whether {n : P(n+1) > P(n)·n^α} has a density for every α — is answered by the paper's own weak-convergence step, and counts to 10¹⁰. The theorem is OpenAI's.