Ordinary two-point correlations and the corrected Elliott conjecture

1 paperLeanreasoning

Proves the ordinary two-point Chowla conjecture, with a bound \(O(X/(\log X)^c)\) for Liouville correlation sums along fixed nonproportional affine forms, where c > 0 is absolute. More generally, proves the binary corrected Elliott conjecture for complex multiplicative functions bounded by one when one factor is uniformly nonpretentious against each fixed Dirichlet character times \(n^{it}\) for \(|t|\le X\).

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Ordinary two-point correlations of multiplicative functions

OpenAI · September 24, 2026

We prove the ordinary two-point Chowla conjecture. For every fixed pair of nonproportional affine forms, the Liouville correlation has a power-of-logarithm saving at every cutoff, with an absolute exponent. We also prove the binary corrected Elliott conjecture for ordinary averages of complex multiplicative functions of modulus at most one, under uniform nonpretentiousness of at least one original factor. This qualitative conclusion holds in fixed residue classes and for fixed nonproportional affine forms.

Read PDF Download Source

Cite

@misc{OAI:Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026,
  author = {{OpenAI}},
  title = {{Ordinary two-point correlations of multiplicative functions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026/final.pdf}{OAI:Ordinary-two-point-correlations-of-multiplicative-functions-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):

Ordinary two-point correlations of multiplicative functions

Scope

The formalization proves ordinary two-point cancellation for multiplicative functions. For the Liouville function on every fixed pair of nonproportional affine forms, the correlation sum up to \(X\) is \(O(X/(\log X)^c)\) for an absolute \(c>0\), with the implied constant depending on the forms.

For two one-bounded multiplicative functions, if at least one is uniformly nonpretentious against all Dirichlet-character twists with frequency \(|t|\le N\), then their shifted and nonproportional affine correlation sums divided by \(N\) tend to zero. These are ordinary averages, with no logarithmic averaging.

Comparator links

Result	Comparator statement
Ordinary Elliott cancellation under uniform nonpretentiousness	OrdinaryElliott.lean
Ordinary Liouville and multiplicative two-point correlations	OrdinaryTwoPointCorrelations.lean

Scope note on GitHub →

Reasoning summary

OpenAI released an abridged summary of the model's reasoning for this result: Ordinary two-point correlations of multiplicative functions (PDF).