On the paucity of lattice triangles

A rational triangle $T$ (one whose angles are rational multiples of $\pi$) unfolds to a translation surface $(X_T,{\omega }_T)$. The lattice triangle problem asks to classify those $T$ for which $(X_T,{\omega }_T)$ is a Veech (lattice) surface, which means that the ${\mathrm{SL}}_2(\mathbb{R})$-orbit of $(X_T,{\omega }_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 \mathrm{/}2,2\pi \mathrm{/}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).