On the paucity of lattice triangles
David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang
math.DS
Mar 25, 2026 · v1
TL;DR
AxiomProver autoformalized the paper's main engine in Lean using mathlib.
Abstract
A rational triangle $T$ (one whose angles are rational multiples of $π$) unfolds to a translation surface $(X_T,ω_T)$. The lattice triangle problem asks to classify those $T$ for which $(X_T,ω_T)$ is a Veech (lattice) surface, which means that the $\operatorname{SL}_2(\mathbb R)$-orbit of $(X_T,ω_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 density 0 subset of the triangles in this window. The main engine in this paper was autoformalized by AxiomProver in Lean (using mathlib).
Problem
The lattice triangle problem asks which rational triangles unfold to Veech (lattice) translation surfaces. In the hard obtuse window (largest angle in (pi/2, 2pi/3]), it is conjectured that no lattice triangles exist, but proving this for all triangles in the window remained open.
Approach
Using an arithmetic reformulation of the Mirzakhani-Wright rank obstruction, the authors prove a quantitative theorem ruling out all but a density-0 subset of triangles in the hard obtuse window. The main engine of the proof was autoformalized by AxiomProver in Lean using Mathlib.
Results
The paper rules out all but a density-0 set of triangles in the hard obtuse window as potential lattice triangles, providing strong quantitative evidence for the conjecture that no lattice triangles exist in this regime.
