AI Proved What?

Episode 007, October 2026

Even or odd

Ordinary two-point correlations and the corrected Elliott conjecture

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

Play Episode 007: Even or odd? Chowla’s conjecture. The integers 1 to 64 colored blue or orange by whether they have an even or odd number of prime factors.

7:51. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Even or odd
  2. 0:55The Liouville function
  3. 1:47Chowla’s conjecture
  4. 2:34What was known
  5. 3:18Two kinds of average
  6. 3:57The claim
  7. 4:48Inside the proof
  8. 6:50Lean, and the caveats

The claim, in plain words

Write Ω(n) for the number of prime factors of n, counted with repeats, and λ(n) = (−1)Ω(n): +1 when the count is even, −1 when it is odd. This is the Liouville function. In 1965 Sarvadaman Chowla conjectured that λ at nearby integers behaves like independent coin flips. The two-point case says that for every fixed gap h ≥ 1, the sum of λ(n)λ(n + h) over n ≤ X is o(X): in the limit, n and n + h have the same parity exactly half the time.

Result 007 claims this with a rate, at every scale. For any two fixed linear forms a1n + b1 and a2n + b2 that aren’t proportional, |Σn≤X λ(a1n + b1)λ(a2n + b2)| ≤ C·X/(log X)c for all X ≥ 3, where c > 0 is the same for every pair of forms and C depends on the forms. It also claims the binary corrected Elliott conjecture for ordinary averages: for multiplicative f1, f2 bounded by 1, one of which stays far from every Dirichlet character twisted by nit uniformly in |t| ≤ N, the average of f1(n + h1)f2(n + h2) tends to 0.

What it doesn’t claim

It covers pairs only: Chowla’s conjecture for three or more points, in ordinary averages, is still open. The general Elliott theorem comes with no rate. The exponent c is absolute but tiny: from the paper’s own parameter choices it is below 2 × 10−14, so at X = 10100 the factor (log X)c is less than 1 + 10−13. The paper says its constants need not be effective. So the bound says nothing you could check numerically; it is a statement about the limit. And it is not a twin prime result: the two problems are often compared, but neither is known to imply the other.

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 Lean proofs of both main theorems (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and the paper is unchanged since the repository’s first public version. As recently as August 26, 2026, a paper on the topic (arXiv:2608.23500) described the two-point conjecture as open “even at h = 1.” We found no public critique specific to this result.

What was known

  • Matomäki and Radziwiłł (2015; Annals 2016): for each h, the normalized correlation stays below 1 − δ(h) in size.
  • Matomäki, Radziwiłł and Tao (2015): the conjecture on average over gaps h ≤ H, for any H → ∞. Their short-interval estimates are an input to the new proof.
  • Tao (2015; Forum of Mathematics, Pi 2016): the logarithmically averaged version, with weight 1/n, which he used to settle the Erdős discrepancy problem.
  • Helfgott and Radziwiłł (2021) and Pilatte (2023; JAMS 2026): quantitative rates for the logarithmic version at h = 1, by divisibility-graph expansion.
  • Tao and Teräväinen (2018; Algebra & Number Theory 2019): ordinary averages vanish outside a set of scales of logarithmic density zero; later quantitative versions (2025) still allow exceptional scales.

How the proof goes

  1. Dilations. λ is completely multiplicative and λ(d)² = 1, so λ(dn)λ(dn + dh) = λ(n)λ(n + h). Comparing the pair (n, n + h) with (dn, dn + dh) leads to a graph on the integers with edge displacement hd. Each copy lives at a different scale, so the paper groups multipliers of nearly equal size.
  2. Centering. Each divisibility indicator splits as 1/p plus a correction 1p|n − 1/p with mean zero. Short-interval Fourier estimates of Matomäki, Radziwiłł and Tao show the averaged parts contribute little; what remains is a graph operator with centered weights, bounded through closed walks.
  3. Prime supplies. Each step uses one prime from each of J disjoint supplies of reciprocal mass about W. The mass is at least WJ, while the operator bound is (C√W)J with an absolute C, so the ratio decays like (C/√W)J. With J growing like log log X, that is a power-of-log saving.
  4. Finite scales. The supplies’ residues are not truly independent inside one interval. The residue tests are encoded as constant-depth Boolean circuits and compared with independent residues using Braverman’s 2010 theorem that polylogarithmic independence fools such circuits. A forest encoding counts the patterns of repeated primes.
  5. General functions. For the Elliott theorem there is no rate to exploit. The paper fixes an auxiliary scale, uses two bands of primes with different weights, and derives a contradiction from any persistent correlation.

The paper credits the graph method to Helfgott and Radziwiłł and to Pilatte. OpenAI also released an abridged summary of the model’s reasoning for this result, one of ten such summaries. It records dead ends, including operator-algebra and adelic approaches and a polynomial substitution, before the return to divisor graphs.

The Lean statement

theorem liouville_log_saving :
    ∃ c : ℝ, 0 < c ∧ ∀ a₁ a₂ b₁ b₂ : ℕ,
      0 < a₁ → 0 < a₂ → a₁ * b₂ ≠ a₂ * b₁ →
      ∃ C : ℝ, 0 < C ∧ ∀ X : ℝ, 3 ≤ X →
        ‖affineSum liouville liouville
            a₁ a₂ b₁ b₂ ⌊X⌋₊‖ ≤
          C * X / Real.rpow (Real.log X) c

This is one of three statements in the challenge file that OpenAI’s setup checks with the Comparator tool; the other two are the Elliott theorems, which also have a separate challenge. Here liouville is defined from Mathlib’s ArithmeticFunction.liouville, and c is chosen before the forms, so it is absolute. A passing check guarantees that the proof proves exactly these statements, using only Lean’s standard axioms (propext, Quot.sound, Classical.choice). The OpenAI-written files behind this challenge come to 1,539 files and 153,427 lines; the separate Elliott challenge adds 628 files and 70,806 lines. A search found no sorry and no new axioms, but a search is not a substitute for running the check, and we have not run it. OpenAI says its papers and proof files were produced by an internal AI model; its catalog of formal proofs does not yet list these.

The numbers in the video

  • From our sieve of Ω(n) mod 2 up to 108: Σn≤108 λ(n)λ(n + 1) = −3,916, so neighbors match 49,998,042 times out of 100,000,000 (49.998%). For gaps 2 and 3 the sums are 4,632 and 10,714. Fair coins would typically give an imbalance on the order of √108 = 10,000.
  • The running sum L(X) = Σn≤X λ(n) is −94 at 104, −530 at 106 and −3,884 at 108, and never exceeds 0 on [2, 108]. Pólya’s guess that it never does fails first at 906,150,257 (Tanaka, 1980).
  • The toy sequence (−1)⌊ln n⌋ has logarithmic average tending to 0 (0.047 at 108), while its ordinary average keeps swinging to about ±(e − 1)/(e + 1) ≈ ±0.462.
  • For the character mod 3 (1, −1, 0, 1, −1, 0, …), the product of neighbors averages −1/3.
  • The bound on c: c = δ/(6WA) with δ = 1/200 and A ≥ 1000, and the paper’s choice of W forces W ≥ e12 · 288 ≈ 4.7 × 107.

Read the source

The paper

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

Transcript

Read the full script

0:00Even or odd

Take any whole number and break it into primes. Twelve is two times two times three: three prime factors, an odd count. Ten is two times five: an even count. Color every number by that parity, blue for even and orange for odd. Now look at neighbors. Does the parity of n tell you anything about the parity of n + 1? Up to 100 million, neighbors match 49.998 percent of the time. The imbalance, about 4,000 pairs, is smaller than fair coin flips would typically give. In 1965, Sarvadaman Chowla conjectured that in the limit, the match rate is exactly 1/2, for neighbors and for any fixed gap. As recently as August, a paper called this two-point case open, even for neighbors. Result 007 in OpenAI’s math repository claims to prove it, with a Lean proof attached.

0:55The Liouville function

This coloring is the Liouville function. λ(n) is plus one when n has an even number of prime factors, counted with repeats, and minus one when the count is odd. It’s completely multiplicative: λ(mn) = λ(m)·λ(n). Add up λ, and you get a running tally: even minus odd. Landau showed that the prime number theorem is equivalent to this tally growing more slowly than n itself. The Riemann hypothesis is equivalent to it growing no faster than roughly the square root of n. So λ alone already encodes the primes. It can fool you, too. Pólya guessed that, from 2 on, the tally never goes above zero. Up to 100 million, it never does. But it fails, for the first time, at 906,150,257.

1:47Chowla’s conjecture

Chowla’s conjecture is about patterns. Multiply λ(n) by λ(n + h), and add up for n up to X. If the parities behaved like independent coins, the total would be tiny compared with X. The two-point conjecture says it is: for every fixed gap h, the sum is o(X). Chowla’s full conjecture allows any number of points. Why is it hard? Sieve methods, the main tools for studying primes, have a blind spot called the parity problem: they can’t tell an even number of prime factors from an odd number. Chowla’s conjecture is about exactly that parity. It’s often compared to the twin prime conjecture. Neither is known to imply the other, but both ask how the factors of n relate to those of a nearby number.

2:34What was known

In the last decade, the problem was surrounded. In 2015, Matomäki and Radziwiłł showed that neighbors can’t be perfectly correlated, or perfectly anti-correlated. With Tao, they proved the conjecture on average over the gap h. Then Tao proved a weighted version, in which each n counts with weight 1/n. That logarithmic version was strong enough to settle the Erdős discrepancy problem. Helfgott and Radziwiłł, and then Pilatte, gave it quantitative rates, for neighbors. For the plain, unweighted average, Tao and Teräväinen showed cancellation at almost all scales: any exceptional scales must be very sparse. But nobody could rule them out completely.

3:18Two kinds of average

Why does the weighting matter? Here is a sequence that flips sign each time the natural log of n passes a whole number. Its logarithmic average settles down to zero. Its ordinary average never settles: it keeps swinging, to about ±0.46. The ordinary average is dominated by its last stretch. The logarithmic average spreads its weight evenly across scales, so one bad stretch barely registers. As the paper puts it, an ordinary estimate must control the terminal scale itself. Ordinary cancellation implies logarithmic cancellation, but not the other way around.

3:57The claim

Result 007 claims the ordinary version, with a rate. Take two fixed linear forms, a₁n + b₁ and a₂n + b₂, that aren’t proportional. Then the correlation sum up to X is at most a constant times X, divided by (log X) to a power c. The power c is absolute: the same for every pair of forms. The forms n and n + h give Chowla’s two-point conjecture. The paper also proves the binary corrected Elliott conjecture: the same cancellation, without a rate, for any two multiplicative functions bounded by one, provided one of them stays far from every Dirichlet character, even a twisted one, at every large scale, even if the twist changes from scale to scale. Some such condition is needed: the character mod 3 has neighbor correlation −1/3.

4:48Inside the proof

The proof starts from a symmetry. λ(2) is minus one, so doubling both numbers flips both signs, and their product stays the same. λ(5)·λ(6) equals λ(10)·λ(12). The same holds for any multiplier d. So join each multiple of d to the number dh further along. You get a graph on the integers. The correlation becomes a sum over this graph’s edges. Split each divisibility condition into its average, 1/p, plus a correction with mean zero. A short-interval theorem of Matomäki, Radziwiłł and Tao shows that the averaged parts contribute almost nothing, so only the corrections remain. Bounding those means counting closed walks in the graph. Roughly, a prime used only once along a walk averages out to zero, so essentially only walks that reuse their primes survive. Then the bookkeeping. Each step uses J primes, one from each of J separate supplies, each of weight W. The useful mass grows like W^J. The cost grows only like a constant times √W, to the J. That leaves a gain of √W, up to a constant, J times over. With J growing like log log X, the gain becomes a power of log X. At any finite scale, the primes’ residues aren’t truly independent. For that, the paper borrows a 2010 theorem from computer science, Braverman’s: shallow circuits, of constant depth, can’t tell limited independence from true randomness. A forest encoding handles repeated primes. The general Elliott case uses a different graph argument, by contradiction, with no rate. OpenAI released a summary of the model’s reasoning for this result, one of ten such summaries. It shows dead ends: operator algebras, adelic kernels, a polynomial substitution. Then it returned to divisor graphs, modeled on the work of Helfgott and Radziwiłł, and of Pilatte. The paper credits both.

6:50Lean, and the caveats

Both theorems are stated in Lean, built on Mathlib’s Liouville function. The proof behind these statements runs to about 1,500 files of OpenAI’s code, more than 150,000 lines. A passing Comparator check would guarantee those exact statements, from Lean’s usual axioms. OpenAI’s catalog of formal proofs doesn’t list them yet, and we haven’t run the check ourselves. The caveats. This is a preprint, not peer reviewed. The saving is real, but tiny. By the paper’s own parameter choices, c is below one fifty-trillionth, and the paper doesn’t claim the constant can be computed. So at any size anyone could compute, the bound says almost nothing: it’s a statement about the limit. The general theorem has no rate at all. And Chowla’s conjecture for three or more points, in ordinary averages, is still open. Even and odd, neighbor to neighbor: a fair coin, at every scale. 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.