On the paucity of lattice triangles

Abstract

A rational triangle $T$ (one whose angles are rational multiples of $\pi$) 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 ${\mathrm{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 $(\pi /2,2\pi /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).

arXiv commentThe paper is significantly revised based on referee comments. And, Jesse Thorner is added as a co-author