On the paucity of lattice triangles

TL;DR

This paper investigates rational lattice triangles, especially obtuse ones, proving that almost all such triangles in a certain angle range do not produce lattice surfaces, using advanced arithmetic and formal proof methods.

Contribution

It provides a quantitative result ruling out most lattice triangles in the hard obtuse angle regime, utilizing an arithmetic reformulation and formalized proof techniques.

Findings

Almost all triangles in the specified angle range are not lattice.

A density 0 subset of triangles may still be lattice.

Formal proof was achieved using Lean and mathlib.

Abstract

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 $\operatorname{SL}_2(\mathbb R)$-orbit of $(X_T,\omega_T)$ is closed in its stratum (so its projection to moduli space is a Teichm\"uller 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 density 0 subset of the triangles in this window. The main engine in this paper was autoformalized by AxiomProver in Lean (using mathlib).