Aftermath bot: New page: the two-point Chowla conjecture (openai/math family 007): ordinary two-point Chowla with a logarithmic saving and binary corrected Elliott (Lean); public follow-ups: MathVet, atimics/math2 NT-7 and RD-1, cert-machine, con-leche, Wang-Yi arXiv:2610.16394, Lattice24

2026-10-19T15:33:22Z

New page: the two-point Chowla conjecture (openai/math family 007): ordinary two-point Chowla with a logarithmic saving and binary corrected Elliott (Lean); public follow-ups: MathVet, atimics/math2 NT-7 and RD-1, cert-machine, con-leche, Wang-Yi arXiv:2610.16394, Lattice24

New page

'''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 ([https://github.com/openai/math 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''0.
** 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''1, ''a''2 ≥ 1 and ''b''1, ''b''2 ≥ 0 with ''a''1''b''2 − ''a''2''b''1 ≠ 0, |Σ1≤''n''≤''X'' λ(''a''1''n'' + ''b''1)λ(''a''2''n'' + ''b''2)| ≤ ''C'' ''X''/(log ''X'')''c'' for every real ''X'' ≥ 3, with ''C'' depending on the forms. The manuscript states that the case ''a''1 = ''a''2 = 1, ''b''1 = 0, ''b''2 = ''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''1, ''f''2 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''1(''n'' + ''h''1)''f''2(''n'' + ''h''2) → 0 for all fixed distinct ''h''1, ''h''2 ≥ 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026 Ordinary two-point correlations of multiplicative functions] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/007.md 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 <code>OrdinaryElliott.lean</code> and <code>OrdinaryTwoPointCorrelations.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 (''a''1, ''a''2 > 0, ''b''1, ''b''2 ≥ 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 <code>OrdinaryElliott</code> and no machine check for <code>OrdinaryTwoPointCorrelations</code>, 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 || [https://github.com/atimics/math2/blob/2c0f00528a8bb375d02bd48a513062254a53c285/docs/COROLLARIES.md atimics/math2], ''Cross-family corollaries of openai/math'', entries NT-7 and RD-1 (GitHub, commit <code>2c0f005</code>) || Use (conditional corollaries, in Lean) || Entry NT-7 proves in Lean, assuming the comparator statement <code>liouville_log_saving</code>, that #{1 ≤ ''n'' ≤ ''X'' : λ(''a''1''n'' + ''b''1) = λ(''a''2''n'' + ''b''2)} = ''X''/2 + ''O''(''X''/(log ''X'')''c''), so that Ω(''a''1''n'' + ''b''1) and Ω(''a''2''n'' + ''b''2) agree in parity for half of all ''n''. Entry RD-1 proves in Lean that the two binary corrected Elliott comparator statements, in <code>OrdinaryTwoPointCorrelations</code> and <code>OrdinaryElliott</code>, 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 || [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/OrdinaryTwoPointCorrelations.json cert-machine], openai/math lane K, run 38019899278 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>OrdinaryTwoPointCorrelations</code> solution (2,531 s) and the [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/OrdinaryElliott.json <code>OrdinaryElliott</code>] 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>OrdinaryElliott</code> or <code>OrdinaryTwoPointCorrelations</code>, 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'', [https://arxiv.org/abs/2610.16394v1 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 ''a''1, ''a''2, ''b''1, ''b''2 with ''a''1''b''2 − ''a''2''b''1 ≠ 0, the ordinary average of ''a''(Ω(''a''1''n'' + ''b''1), Ω(''a''2''n'' + ''b''2)) agrees with (1/''N''2)Σ''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 e''i''θΩ(''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 [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_066.json rank_066] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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.

[[Category:OpenAI results]]

The two-point Chowla conjecture - Revision history

Aftermath bot: New page: the two-point Chowla conjecture (openai/math family 007): ordinary two-point Chowla with a logarithmic saving and binary corrected Elliott (Lean); public follow-ups: MathVet, atimics/math2 NT-7 and RD-1, cert-machine, con-leche, Wang-Yi arXiv:2610.16394, Lattice24