Papers With

← All papers
First page of On the paucity of lattice triangles

On the paucity of lattice triangles

David Kurniadi Angdinata, Evan Chen, Ken Ono, Jesse Thorner, Jiaxin Zhang, Jujian Zhang

math.DS Mar 25, 2026 · v2 math.CO math.NT
autoformalization ai-agents mathlib number-theory
Read PDF arXiv abstract Code
TL;DR
AxiomProver autoformalized and verified in Lean with Mathlib the paper's main analytic number theory estimate, a lower bound for the counting sum S(p,q).
Abstract
A rational triangle $T$ (one whose angles are rational multiples of $π$) unfolds to a translation surface ${X_T}$. The lattice triangle problem asks to classify those $T$ for which ${X_T}$ is a Veech (lattice) surface, which means that the $\operatorname{SL}_2(\mathbb R)$-orbit of ${X_T}$ is closed in its stratum (so its projection to moduli space is a Teichmüller curve). The most mysterious regime is the "hard obtuse window" (largest angle in $(π/2,2π/3]$), where it is conjectured that no lattice triangles exist. Using an arithmetic reformulation of the Mirzakhani-Wright rank obstruction, we prove a quantitative theorem that rules out all but a proportion $n^{-1+o(1)}$ of the triangles in this window with denominator $n$. The main technical result in our proof was autoformalized by AxiomProver in Lean (using mathlib).
Problem

The lattice triangle problem asks which rational triangles unfold to Veech surfaces. In the hard obtuse window (largest angle in (π/2, 2π/3]) no lattice triangles are conjectured to exist. The goal is to rule out almost all triangles in this window with denominator n.

Approach

The Mirzakhani–Wright rank obstruction, in the number-theoretic form of Larsen–Norton–Zykoski, reduces the problem to finding a usable unit a mod n satisfying two modular inequalities. The authors count such units with a sum S(p,q), expand it via discrete Fourier analysis into Ramanujan sums, and bound the error term using the vanishing of Ramanujan sums when n has a large prime factor. The main analytic estimate, Theorem 6.1, was autoformalized in Lean/Mathlib by AxiomProver from a natural-language draft. During formalization AxiomProver also corrected mistakes in that draft.

Results

For n with a sufficiently large prime factor, all but a vanishing proportion of candidate triangles fail the lattice property. Overall, all but a proportion n^{-1+o(1)} of triangles in the window are excluded. The key lower bound S(p,q) ≥ 5 for almost all pairs was formally verified in Lean, while deep external results such as the rank obstruction were taken as given.