In 2014, Maryam Mirzakhani became the first woman ever to win the Fields Medal, the highest honor in mathematics. She had come from Tehran to Harvard and then Stanford, and by then she had already changed several areas of geometry and dynamics. Those who knew her often remarked on how she worked: slowly, visually, by drawing and redrawing surfaces until the hidden structure came into focus. That style matters for this story because the problem in our new paper lies precisely in the world she helped illuminate.
To a non-mathematician, "the dynamics and geometry of Riemann surfaces and their moduli spaces" can sound impossibly abstract. But one way into that world is unexpectedly concrete: imagine a billiard ball moving on a polygonal table. On a rectangle, the motion is familiar. On a triangle, things quickly become mysterious. Does the path repeat? Does it wander everywhere? Are there deep, hidden symmetries? Questions that look like recreational geometry turn out to touch some of the deepest ideas in modern mathematics.
Mirzakhani’s importance lies partly in showing how much order lies hidden within that apparent chaos. In her early work, she learned how to count simple closed geodesics, the closest thing curved surfaces have to straight closed loops. She used those ideas to reveal large-scale structure in the "moduli spaces" that parametrize all possible shapes of a surface. This is the essence of Teichmüller theory.
Later, with Alex Eskin and Amir Mohammadi, she helped prove a spectacular rigidity theorem: in the world of translation surfaces, orbit closures that might have looked hopelessly wild are in fact far more structured than anyone expected. Anton Zorich famously called this the "Magic Wand" theorem. It gave researchers a way to move from isolated examples to a real theory.
From billiards to translation surfaces
Here is the visual trick behind the subject. Suppose a billiard ball hits a side of a triangle. Instead of letting the path bounce, reflect the whole triangle across that side. In the reflected copy, the path keeps going in a straight line. Repeat this every time the ball hits a wall. The broken billiard path becomes a straight path through a hall of mirror images.
If the triangle’s angles are rational number multiples of π, only finitely many orientations can appear. So, one can glue all the mirror copies together along matching sides. The result is a new geometric object called a translation surface. On that surface, the billiard problem has been converted into the problem of understanding straight-line motion. This is one of the great ideas in the field: a question about bouncing becomes a question about geometry.
William Veech discovered that some of these translation surfaces are extraordinarily rigid. They have so much hidden symmetry that the straight-line flow behaves in a beautifully organized way. In the language of the field, these are Veech surfaces, or lattice surfaces. So, when we speak of a "lattice triangle," we do not mean a triangle whose vertices sit on graph paper. We mean a rational triangle whose unfolding produces one of these rare, highly symmetric translation surfaces.
Why triangles are hard
That leads to a natural classification problem: which rational triangles are lattice triangles? This question sits at the intersection of geometry, dynamics, and arithmetic. It has been studied for decades, and yet it remains surprisingly open.
There has been substantial progress. The acute and right-angled cases are understood. In the obtuse world, two infinite families are known, and Hooper discovered a remarkable sporadic scalene example. But the regime that experts still find most mysterious is the obtuse scalene window, the case where all three angles are different and the largest angle lies strictly between 90 and 120 degrees. Many mathematicians believe that no lattice triangles live there at all.
This is where Mirzakhani’s legacy comes into play. A powerful obstruction, arising from the work of Mirzakhani and Alex Wright (University of Michigan), shows that certain geometric configurations cannot occur if a triangle is a lattice. Anne Larsen, Chaya Norton and Bradley Zykoski turned that obstruction into an effective arithmetic criterion and used it to rule out the strongly obtuse regime, where the largest angle is greater than 120 degrees. But the hard window remained.
Alex Wright’s question
Our paper grew out of an email Alex Wright sent to one of us.
"Mathematicians are sure they know all lattice triangles; the problem is to prove all other triangles are not lattice triangles. There are some elementary criteria. The one used in the paper (i.e. by Larsen, Norton, and Zykoski) is just in terms of modular arithmetic. That criterion is not enough on its own to completely finish the problem, but it should be possible to get surprisingly close using just that criterion."
That is exactly the challenge we took up. Could one squeeze much more out of the arithmetic shadow of the Mirzakhani-Wright obstruction?
What we proved
In our paper "On the Paucity of Lattice Triangles," we show that the answer is yes. We do not completely solve the conjecture. But we prove, answering Wright’s question, that in a precise asymptotic sense, that lattice triangles inside that window are extraordinarily rare.
Write a rational triangle’s angles as $\left(\frac{p\pi}{n},\frac{q\pi}{n},\frac{(n-p-q)\pi}{n}\right)$. Now fix the denominator n and look at all candidate obtuse triangles in the hard window with those kinds of angles. Our theorem says that for a density 1 set of denominators n (i.e., for almost all denominators), the proportion of those candidates that can be lattice triangles tends to zero as n grows.
What we prove, informally In plain English: if one looks at larger and larger denominators, then for almost every denominator, almost every candidate triangle in the hard obtuse window fails to have the lattice property. Any surviving examples, if they exist at all, lie in a vanishingly thin exceptional set.
This is not the final classification. But it is a strong quantitative statement. It says that the hard window is not just difficult, it is sparse. The exceptional candidates do not make up a substantial population. They thin out to almost nothing.
What makes this striking is the route we take to get there. The original obstruction comes from geometric ideas about orbit closures on moduli spaces. But once translated into the right arithmetic language, the problem becomes an intricate counting problem about residues modulo n. The heart of the paper is to show that the relevant arithmetic inequalities almost always have a solution, and hence the triangle almost always fails the lattice test.
The mathematics under the hood
The proof is an amalgamation of several themes that, at first glance, do not seem to belong in a billiards problem.
Analytic number theory lets us control how often certain arithmetic configurations can occur.
Fourier analysis rewrites our counting problem in a form where oscillation becomes visible.
Ramanujan sums - special exponential sums tuned to modular arithmetic - detect the arithmetic obstructions.
The theory of smooth numbers tells us that integers with only small prime factors are rare, which is exactly what turns our estimates into a density 1 statement.
This mix of ideas is, to us, part of the beauty of the result. A problem born in geometry travels through billiards and translation surfaces, picks up a criterion from Mirzakhani and Wright, is recast arithmetically by Larsen, Norton, and Zykoski, and is then attacked with Fourier analysis, Ramanujan sums, and classical estimates about prime factors. It is a reminder that modern mathematics advances not only through deep specialization, but also through unexpected bridges.
The AI experiment: AxiomProver’s role
At Axiom Math, we are building AxiomProver as a tool for mathematical research: an AI system that can serve as a genuine thought partner in rigorous mathematics. This paper gave us a beautiful test case.
To be clear about scope, we did not ask AxiomProver to re-prove the deep theorems of Mirzakhani, Wright, Veech, or the general theory of translation surfaces. Those are external pillars on which the paper rests. Instead, we asked it to handle the analytic engine that drives the density result, the quantitative theorem formalized in our paper as Theorem 6.1.
How AxiomProver handled the proof
The inputs. We provided a natural-language statement of the theorem, a short task description, the Lean version specification, and an incomplete proof that contained (unbeknownst to us) some correctable mistakes.
Formalization in Lean. AxiomProver translated the problem into Lean 4.26.0, working inside Mathlib’s formal environment.
Autonomous proof and correction. AxiomProver corrected the fixable issues in the draft and produced a complete machine-checked proof of the analytic engine.
Artifacts. Readers who want the artifacts can find them here:
arXiv: https://arxiv.org/abs/2603.23928
GitHub: https://github.com/AxiomMath/lattice-triangle
After that, the human authors wrote the paper for human readers.
What did we learn?
We learned that AxiomProver can contribute meaningfully not only to the final checking stage, but also to the development and repair of a substantial analytic argument. There is something especially fitting about the arc of this project: it begins with Mirzakhani’s ability to find hidden structure in apparently chaotic geometric worlds, and it ends with a machine helping us formalize a theorem inside one small corner of that world.