AI Proved What?

Episode 012, October 2026

n or n + 1: who wins?

Independent largest prime factors of consecutive integers: the joint Dickman law

Covers result 012 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 012: n or n + 1, who wins? The largest prime factors of neighbors, Erdős problem 371. A scatter plot of log-sizes of the largest prime factors of n and n + 1 for random n near ten million, split by a diagonal into two halves.

5:15. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Two neighbors
  2. 0:52One number at a time
  3. 1:24Two at a time
  4. 1:59What was known
  5. 2:43The claim
  6. 3:10How the proof goes
  7. 4:23Lean, and the caveats

The claim, in plain words

Write P+(n) for the largest prime factor of n. For 1,000,000 = 26 · 56 it is 5; for 1,000,001 = 101 · 9,901 it is 9,901. For a random n, Dickman’s law (1930) says that P+(n) ≤ na with probability tending to ρ(1/a), where ρ is Dickman’s function: about 30.7% for the square root and 4.9% for the cube root.

Result 012 claims that for neighbors these events are independent in the limit. For every fixed 0 < a, b < 1, the proportion of n ≤ x with P+(n) ≤ na and P+(n + 1) ≤ nb tends to ρ(1/a) · ρ(1/b), in ordinary natural density. Because the limiting law is continuous and symmetric, each ordering, P+(n) < P+(n + 1) and the reverse, has density exactly 1/2. That is Erdős problem #371, and the joint law is the independence conjecture of Erdős and Pomerance.

What it doesn’t claim

There is no rate: the law is a limit, and the data approach it slowly (below). The parameters a and b are fixed; no uniformity as they vary is claimed.

Where it stands

Posted as a preprint
OpenAI, dated September 24, 2026; released October 6, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published a Lean proof of the joint law and both orderings (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and we found no public critique. Erdős problem #371 is still listed as open on erdosproblems.com.

What was known

  • Lower bounds for the share of n with P+(n) < P+(n + 1): 0.0099 (Erdős and Pomerance, 1978), 0.05544 (de la Bretèche, Pomerance and Tenenbaum, 2005), 0.1063 and 0.1356 (Wang, 2017 and 2018), 0.2017 (Lü and Wang, 2025) and 0.280 (Yang, preprint). These are floors; the share was not known, unconditionally, to have a limit.
  • Teräväinen (2018) proved the joint law and the ordering 1/2 with logarithmic weights, counting each n with weight 1/n.
  • Tao and Teräväinen (2019) obtained ordinary averages at almost all scales, outside a set of scales of logarithmic density zero. Wang (2021) proved the ordinary law assuming the Elliott–Halberstam conjecture for friable integers.

How the proof goes

  1. Counts instead of the largest prime. The primes between x1/J and x are cut into bands, and independence of the band counts of n and n + 1 gives the joint law. Fourier analysis reduces this to one correlation going to zero, (1/x) Σ g(n) F(n + 1) → 0, with F centered: the same kind of problem as the two-point Chowla conjecture of episode 7.
  2. Amplify. If the correlation does not vanish, a weighted count of factorizations n = am, n + 1 = cl amplifies it, and Cauchy–Schwarz turns it into a positive energy on a graph that joins integers a short shift apart.
  3. Compare with a random model. The graph is compared, in cut norm, with a model in which each auxiliary prime divides independently with probability 1/p, using sampling tools from computer science.
  4. Short intervals. Everything reduces to averages over short intervals, where theorems of Matomäki and Radziwiłł, and of Matomäki, Radziwiłł and Tao, force cancellation, contradicting the positive energy.

The Lean statement

theorem joint_law (a b : ℝ) (ha : 0 < a) (ha1 : a < 1)
    (hb : 0 < b) (hb1 : b < 1) :
    Tendsto (realDensity (fun n =>
      (n.maxPrimeFac : ℝ) ≤ (n : ℝ) ^ a ∧
      ((n + 1).maxPrimeFac : ℝ) ≤ (n : ℝ) ^ b))
      atTop (𝓝 (rho (1 / a) * rho (1 / b)))

theorem increasing_order :
    Tendsto (realDensity (fun n =>
      n.maxPrimeFac < (n + 1).maxPrimeFac)) atTop (𝓝 (1 / 2))

This abridged statement is from the challenge file; a third theorem gives the reverse ordering, and ρ is defined by its delay equation. The proof behind it is about 1,800 files of OpenAI’s code, some shared with episode 7’s proof, about 176,000 lines. A passing Comparator check would guarantee these statements from Lean’s standard axioms. The result is not yet in OpenAI’s formalization catalog, and we have not run the check.

The numbers in the video

  • For 2 ≤ n ≤ 107, n + 1 has the bigger largest prime factor 50.00% of the time (49.9995%); there are no ties, since neighbors are coprime.
  • How often both largest prime factors are at most √n, divided by the product of the two observed rates: 0.70 up to 104, 0.81 up to 105, 0.88 up to 106 and 0.91 up to 107. Independence predicts 1, and the limit of the joint rate is ρ(2)2 ≈ 9.4%.
  • Checked with a short Python script.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00Two neighbors

Here are two neighbors: 1,000,000, and 1,000,001. 1,000,000 is 2⁶ × 5⁶, so its largest prime factor is 5. 1,000,001 is 101 × 9,901. Its largest prime factor is 9,901. This time, the second number wins. Hold this contest for every pair of neighbors up to 10 million, and the second number wins half the time, to four decimal places. Paul Erdős asked whether it is exactly one half in the limit. The question is listed as Erdős problem #371. Result 012 in OpenAI’s math repository claims to prove it, and more: the sizes of the largest prime factors of two neighbors behave like independent random draws. And it comes with a Lean proof.

0:52One number at a time

First, one number at a time. Measure the largest prime factor on a log scale: its logarithm, divided by the logarithm of n. Karl Dickman found the law of this measure in 1930. The largest prime factor is at most the square root of n for about 31% of numbers, in the limit, and at most the cube root for about 5%. In general, the chance that it is at most n^a tends to ρ(1/a), where ρ is Dickman’s function.

1:24Two at a time

Now two at a time. Neighbors share no prime factor, so you might expect their factorizations to be unrelated. If the largest prime factors of n and n + 1 were independent, the chance that both are at most the square root would be ρ(2)²: about 9%. And by symmetry, each would beat the other half the time. The data lean that way, slowly. Up to 10,000, both are small only 70% as often as independence would predict from the observed rates. Up to 10 million, it is 91%, and still climbing.

1:59What was known

In 1978, Erdős and Carl Pomerance proved that each ordering happens for a positive proportion of numbers: at least about 1%. Later work raised that floor, to 5.5%, then about 11%, 14%, 20%, and 28% in a recent preprint. But these were floors. No one had shown, unconditionally, that the proportion even settles down. Other results changed the averaging. In 2018, Joni Teräväinen proved the full independence with logarithmic weights, counting each n with weight 1/n. Terence Tao and Teräväinen then reached ordinary averages, but only at almost all scales: there could be rare ranges of x where it fails.

2:43The claim

Result 012 claims the ordinary version, at every large scale. For any fixed a and b between zero and one, the proportion of n up to x with P⁺(n) ≤ n^a, and P⁺(n + 1) ≤ n^b, tends to ρ(1/a) × ρ(1/b). That is independence, exactly as predicted. The limiting law is continuous, so ties don’t matter, and symmetry gives one half for each ordering.

3:10How the proof goes

First, trade the largest prime for counts. Cut the primes between x^(1/J) and x into bands, and count how many prime factors of n land in each band. Independence of these counts, for n and n + 1, gives the joint law. By Fourier analysis, that comes down to one correlation going to zero: a function of n’s band counts, times a centered function of n + 1’s, averaged up to x. It is the same kind of problem as Chowla’s conjecture, from episode 7. Suppose the correlation doesn’t vanish. The paper amplifies it by counting ways to factor n and n + 1 with chosen pieces, and Cauchy–Schwarz turns it into a positive energy on a graph that joins integers a short shift apart. It compares that graph with a random model, in which each auxiliary prime divides independently, with probability 1/p, using sampling tools from computer science. In the end, everything reduces to averages over short intervals, where theorems of Kaisa Matomäki and Maksym Radziwiłł, one with Terence Tao, force cancellation. That contradicts the positive energy, so the correlation must vanish.

4:23Lean, and the caveats

Lean. The joint law and both orderings are stated in Lean, with Dickman’s function built from its delay equation. The proof behind them is about 1,800 files of OpenAI’s code, some shared with episode 7’s proof: about 176,000 lines. A passing Comparator check would guarantee those statements from Lean’s usual axioms. OpenAI’s catalog of formal proofs doesn’t list it yet, and we haven’t run the check ourselves. The caveats. This is a preprint, 84 pages, not peer reviewed. The law is a limit, with no rate, and the data show convergence is slow. And Erdős problem #371 is still listed as open. Two neighbors, two largest primes: a fair contest, in the limit. If the proof holds. And a computer can check it.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.