On monic abelian cubic polynomials

Shubhrajit Bhattacharya and Andrew O’Desky

Lean formalization of our count of monic integral cubic polynomials with Galois group \(C_3\), ordered by root height. The number of such polynomials of height at most \(H\) is

\[ H^3P(\log H)+O_\varepsilon(H^{2+\varepsilon}), \]

where \(P\) is an explicit linear polynomial. The proof passes through integral points on a toric cubic surface and the Fourier expansion of its height zeta function.

Read the blueprint · Explore the dependency graph · Browse the Lean source

The paper and the formalization

This project follows our November 2026 revision, including the results for arbitrary trace and Appendices A and B. The arXiv version has the older title On monic abelian trace-one cubic polynomials.

The main counting proofs use Poisson summation and the critical-line mean-square estimate of Chandrasekharan and Narasimhan as explicit hypotheses. For the strip estimate and coefficient sum, Lean retains direct proofs by the residue theorem and Perron’s formula. For the moduli theorem, we formalize the rational-point correspondence used in counting.

The correspondence record describes these choices and the separate literature inputs used in the Santens comparison and the alternative ideal count.

Build

The project uses Lean 4.28.0 and Mathlib. From formalization/, run lake exe cache get followed by python3 scripts/check.py. The check compiles the library, checks the registered statements and proof files, and verifies that all project declarations use only Lean’s standard axioms.