Independent largest prime factors of consecutive integers

1 paperLean

Resolves the Erdős–Pomerance joint Dickman conjecture: the logarithmic sizes of the largest prime factors of n and \(n+1\) are asymptotically independent in ordinary natural density. In particular, the integers satisfying \(P^+(n)\lt P^+(n+1)\) have density 1/2.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The joint Dickman law for consecutive integers

OpenAI · September 24, 2026

Let \(P^+(n)\) denote the largest prime factor of n. We prove that \(\log P^+(n)/\log n\) and \(\log P^+(n+1)/\log n\) are asymptotically independent in ordinary natural density, with Dickman marginals. This resolves the Erdős–Pomerance joint Dickman conjecture positively and implies that the ordering \(P^+(n)\lt P^+(n+1)\) has natural density 1/2.

Read PDF Download Source

Cite

@misc{OAI:The-joint-Dickman-law-for-consecutive-integers-September-24-2026,
  author = {{OpenAI}},
  title = {{The joint Dickman law for consecutive integers}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-joint-Dickman-law-for-consecutive-integers-September-24-2026/paper.pdf}{OAI:The-joint-Dickman-law-for-consecutive-integers-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The joint Dickman law for consecutive integers

Scope

Let \(P^+(n)\) be the largest prime factor of \(n\). The formalization proves the joint Dickman law in ordinary natural density: for every \(0<a,b<1\), the density of integers satisfying \(P^+(n)\le n^a\) and \(P^+(n+1)\le n^b\) tends to \(\rho(1/a)\rho(1/b)\), where \(\rho\) is the Dickman function.

It also proves that each of the orderings \(P^+(n)<P^+(n+1)\) and \(P^+(n+1)<P^+(n)\) has natural density \(1/2\).

Comparator links

Result	Comparator statement
Joint Dickman law and equal ordering densities for consecutive integers	JointDickman.lean

Scope note on GitHub →