The two-point Chowla conjecture

The two-point Chowla conjecture asserts that, for every fixed shift h ≥ 1, the values of the Liouville function λ(n) = (−1)^Ω(n), where Ω(n) counts the prime factors of n with multiplicity, are asymptotically uncorrelated at n and n + h in ordinary averages: (1/X)Σ_n≤X λ(n)λ(n + h) → 0. It is the binary case of Chowla's 1965 conjecture, and Elliott's conjecture extends it to bounded multiplicative functions. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026, claims the conjecture with a power-of-logarithm saving, together with the binary corrected Elliott conjecture for ordinary averages. The collection includes a Lean formalization of both. This page summarizes the published claims 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:
  • Chowla's conjecture predicts vanishing Liouville correlations at every fixed collection of distinct shifts. Elliott extended the problem to bounded multiplicative functions, and Matomäki, Radziwiłł and Tao showed that Elliott's original condition needs correction for complex functions; their corrected condition is the uniform nonpretentiousness used below.
  • Matomäki and Radziwiłł bounded each fixed-shift Liouville correlation by 1 − δ(h) at all large cutoffs, and Matomäki, Radziwiłł and Tao proved cancellation averaged over arbitrarily slowly growing windows of shifts.
  • For logarithmic averages, Tao proved the binary corrected Elliott theorem for nonproportional affine forms. For the logarithmically weighted sum Σ_n≤x λ(n)λ(n+1)/n, Helfgott and Radziwiłł obtained the bound log x/(log log x)^1/2 by divisibility-graph expansion, and Pilatte improved it to (log x)^1−c₀.
  • For ordinary averages, Tao and Teräväinen obtained binary cancellation outside a set of scales of logarithmic density zero, Klurman, Mangerel and Teräväinen relaxed the hypothesis to nonpretentiousness against each fixed twist χ(n)n^it, with cancellation along a set of scales of full upper logarithmic density, and later quantitative estimates of Tao and Teräväinen give logarithmic savings outside a controlled exceptional set of scales.

The original results

• Claim (Liouville correlations). Theorem 1.1 of Ordinary two-point correlations of multiplicative functions states that there is an absolute constant c > 0 such that, for all fixed integers a₁, a₂ ≥ 1 and b₁, b₂ ≥ 0 with a₁b₂ − a₂b₁ ≠ 0, |Σ_1≤n≤X λ(a₁n + b₁)λ(a₂n + b₂)| ≤ C X/(log X)^c for every real X ≥ 3, with C depending on the forms. The manuscript states that the case a₁ = a₂ = 1, b₁ = 0, b₂ = h resolves the ordinary two-point Chowla conjecture, that the implied constants need not be effective, and that no uniformity is asserted for coefficients growing with X.
• Claim (binary corrected Elliott). Theorem 1.2 states that if f₁, f₂ are multiplicative functions with values in the closed unit disc and at least one satisfies inf_|t|≤N D(f, χn^it; N) → ∞ for every fixed Dirichlet character χ, then (1/N)Σ_n≤N f₁(n + h₁)f₂(n + h₂) → 0 for all fixed distinct h₁, h₂ ≥ 0. Corollary 1.3 gives the same conclusion for nonproportional affine forms. No rate is claimed for this class of functions.
• Method, as described: comparing the correlations at n, n + h and at dn, d(n + h) leads to a divisibility graph, adapting the graph methods of Helfgott–Radziwiłł and Pilatte, with the short-interval estimates of Matomäki, Radziwiłł and Tao. In the quantitative argument each step uses one prime from each of J disjoint prime supplies, with J proportional to log log X and centered factors 1_p|n − 1/p; the residue tests are compared with independent residues through Braverman's bounded-independence theorem for constant-depth circuits, after a correction to exact bounded independence in the style of Alon, Goldreich and Mansour. For general multiplicative functions the graph is fixed at an auxiliary scale before the long average is taken.
• Source. The manuscript Ordinary two-point correlations of multiplicative functions at commit 1581d4c.
• Formalization, as described by the repository. The scope note states that the formalization proves the Liouville bound O(X/(log X)^c) on every fixed pair of nonproportional affine forms with an absolute c > 0, and, for one-bounded multiplicative functions with one factor uniformly nonpretentious against all Dirichlet-character twists with |t| ≤ N, that the shifted and nonproportional affine correlation sums divided by N tend to zero, for ordinary averages. The Comparator statements are OrdinaryElliott.lean and OrdinaryTwoPointCorrelations.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". Its note finds no issue beyond observing that the affine forms take natural-number coefficients (a1, a2 > 0, b1, b2 ≥ 0), "which loses nothing up to re-indexing", and that the custom nonpretentiousness definition was checked against the standard one. It records a sandboxed Comparator pass for OrdinaryElliott and no machine check for OrdinaryTwoPointCorrelations, which uses the external packages PrimeNumberTheoremAnd and StrongPNT.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08	atimics/math2, Cross-family corollaries of openai/math, entries NT-7 and RD-1 (GitHub, commit 2c0f005)	Use (conditional corollaries, in Lean)	Entry NT-7 proves in Lean, assuming the comparator statement liouville_log_saving, that #{1 ≤ n ≤ X : λ(a1n + b1) = λ(a2n + b2)} = X/2 + O(X/(log X)c), so that Ω(a1n + b1) and Ω(a2n + b2) agree in parity for half of all n. Entry RD-1 proves in Lean that the two binary corrected Elliott comparator statements, in OrdinaryTwoPointCorrelations and OrdinaryElliott, are equivalent, and that the affine statement implies both.	Repository catalogue; it states that every entry is conditional on the OpenAI claims it cites, and marks NT-7 as rechecked by two independent agents.
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 OrdinaryTwoPointCorrelations solution (2,531 s) and the OrdinaryElliott solution (1,724 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 OrdinaryElliott or OrdinaryTwoPointCorrelations, so the challenges were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-12	B. Wang and S. Yi, Dynamical generalizations of the two-point Chowla conjecture, arXiv:2610.16394	Extension	Proves the two-point case of Charamaras and Richter's conjecture on the asymptotic independence of Ω at consecutive integers: for fixed positive integers a1, a2, b1, b2 with a1b2 − a2b1 ≠ 0, the ordinary average of a(Ω(a1n + b1), Ω(a2n + b2)) agrees with (1/N2)Σm,n≤N a(Ω(m), Ω(n)) up to an error O(‖a‖∞(log log log N)5/2/(log log N)1/2), for every bounded a. As a consequence, (1/N)Σn≤N f(TΩ(n)+Ω(n+1)x) → ∫f dν in every uniquely ergodic system. The proof extends the manuscript's correlation bound in progressions to the functions eiθΩ(n), uniformly in the phases, using its Proposition 2.1, Lemmas 2.2, 4.2 and 4.6 and Proposition 8.4.	arXiv preprint, version 1 (19 pages).
2026-10-16	J. Jardine, Lattice24, referee review rank_066 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap. The reviewer states that it read the quantitative Part I closely and much of the qualitative Part II, and only skimmed four files of Part II. Its one minor note is that the truncated inclusion–exclusion in the rough-number sieve needs a scale parameter of the argument to exceed roughly e3000; it states that this is valid as an asymptotic statement and not a gap, but makes the threshold and the implied constants astronomically large and ineffective, which the manuscript acknowledges.	Part of an audit that its repository describes as a complete review of the collection's manuscripts without a Lean formalization; this manuscript is in its results table. The reviews are published under CC BY 4.0.

Notes

• The logarithmically averaged results and the earlier ordinary-average 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.