Patterson's first moment for cubic Gauss sums

1 paperLean

Proves unconditionally the all-primary-prime form of Patterson’s first-moment asymptotic: normalized cubic Gauss sums over primary Eisenstein primes of norm at most X, including both conjugates, have an explicit positive main term of order \(X^{5/6}/\log X\). Every fixed nonzero prime-angle Fourier mode has smaller order.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 1

An unconditional first moment for cubic Gauss sums

OpenAI · September 25, 2026

We prove Patterson's first-moment conjecture for normalized cubic Gauss sums over all primary Eisenstein primes, unconditionally. The sharp-cutoff main term is \((6/5)c_*X^{5/6}/\log X\), where \(c_*=(2\pi)^{2/3}/(3\Gamma(2/3))\). For every fixed nonzero angular Fourier mode of the prime argument, we also prove cancellation at the first-moment scale.

Read PDF Download Source

Cite

@misc{OAI:An-unconditional-first-moment-for-cubic-Gauss-sums-September-25-2026,
  author = {{OpenAI}},
  title = {{An unconditional first moment for cubic Gauss sums}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-unconditional-first-moment-for-cubic-Gauss-sums-September-25-2026/paper.pdf}{OAI:An-unconditional-first-moment-for-cubic-Gauss-sums-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

An unconditional first moment for cubic Gauss sums

Scope

Patterson's first-moment conjecture concerns the average of normalized cubic Gauss sums over primary Eisenstein primes. The formalization proves the sharp-cutoff asymptotic with main term \(\frac65c_*X^{5/6}/\log X\), where \(c_*=(2\pi)^{2/3}/(3\Gamma(2/3))\). It also proves the corresponding angular comparison for every integer Fourier mode and cancellation of order \(o(X^{5/6}/\log X)\) for each fixed nonzero mode. All primary Eisenstein primes are included, without an extra conjectural premise.

Comparator links

Result	Comparator statement
Patterson first moment and angular cancellation	PattersonFirstMoment.lean

Scope note on GitHub →