On the paucity of lattice triangles

This paper proves that, within the conjectured "hard obtuse window" where no lattice triangles are expected to exist, all but a density-zero subset of rational triangles are ruled out as Veech surfaces, utilizing an arithmetic reformulation of the Mirzakhani-Wright rank obstruction that was autoformalized in Lean.

The Gist

Imagine you are a billiard player, but instead of a standard table, you are playing on a triangular table with very specific, "rational" angles (angles that are neat fractions of a circle, like 1/5th or 1/7th of a full turn).

When you hit a ball on such a table, it bounces around forever. Mathematicians have a clever trick to study this: they "unfold" the triangle. Imagine reflecting the triangle across its sides over and over again, creating a mosaic of triangles that eventually glue together to form a flat, donut-shaped surface (a "translation surface").

The Big Question:
For which of these triangular tables does the ball's path behave in a perfectly predictable, "lattice" way? These special tables are called Lattice Triangles. They are the "gold standard" of billiard dynamics because their paths are highly structured and beautiful.

The Mystery:
Mathematicians have already figured out the rules for "sharp" (acute) and "right-angled" triangles. But the "obtuse" triangles (those with one very wide, lazy angle) are a mess.

• We know a few specific obtuse triangles work.
• We know two infinite families of them work.
• But there is a "Hard Window": a specific range of wide angles (between 90° and 120°) where we suspect no lattice triangles exist at all. It's like a dark room where we think no treasure is hidden, but we can't prove it.

What This Paper Does:
The authors, a team of mathematicians (and an AI assistant), set out to prove that in this "Hard Window," lattice triangles are incredibly rare—so rare that if you picked a random triangle from this group, the chance of it being a lattice triangle is effectively zero.

They didn't just guess; they built a massive mathematical machine to count them.

The Analogy: The "Magic Filter"

Think of the problem like trying to find a specific type of grain of sand on a beach.

1. The Beach: The "Hard Window" of obtuse triangles.
2. The Grains: Every possible triangle in that window.
3. The Goal: Find the "Golden Grains" (the Lattice Triangles).

The authors used a tool called the Mirzakhani-Wright Rank Obstruction. Let's call this the "Magic Filter."

• If a triangle passes through the filter, it might be a Lattice Triangle.
• If it gets stuck in the filter, it is definitely not a Lattice Triangle.

The paper proves that for almost every triangle in the Hard Window, the Magic Filter catches them. The only ones that slip through are so few that they disappear into the background noise as the numbers get bigger.

How They Did It (The Engine)

To prove this, they turned the geometry problem into a number puzzle.

• They created a counting function, let's call it $S(p, q)$. This function counts how many "keys" (mathematical numbers) fit into a specific lock for a given triangle.
• If the count is high enough (specifically, 5 or more), the triangle is disqualified from being a Lattice Triangle.
• They used Fourier Analysis (a way of breaking complex waves into simple ripples) and Ramanujan Sums (a special type of number pattern) to analyze these counts.

The "Large Prime" Trick:
The secret sauce was realizing that if the denominator of the triangle's angle has a very large prime number factor, the math forces the "ripples" to cancel each other out perfectly.

• Imagine a crowd of people clapping. If everyone claps at random times, it's loud and chaotic.
• But if the crowd is organized by a large prime number rule, the clapping cancels out, leaving silence.
• This "silence" (mathematical cancellation) meant the error in their calculation was tiny, proving that the "count" ($S$) was definitely high enough to disqualify the triangle.

The AI Twist: AxiomProver

Here is the most futuristic part of the story.
The core mathematical engine of this proof (Theorem 6.1) was automatically written and verified by an AI system called AxiomProver.

• The Human Role: The human mathematicians wrote a rough draft of the proof and the problem statement.
• The AI Role: The AI took this draft, found small mistakes, fixed them, and translated the entire proof into Lean, a computer language used to verify math with 100% logical certainty.
• The Result: The AI didn't just check the math; it wrote the formal proof. The humans then took that computer code and rewrote it into the English paper you are reading.

The Bottom Line

This paper is a victory for two things:

1. Math: It proves that in the most mysterious, difficult part of the "Lattice Triangle" problem, the answer is almost certainly "No." Lattice triangles are vanishingly rare in this zone.
2. AI: It shows that AI is ready to be a true partner in high-level mathematics, capable of not just checking work, but constructing rigorous, verified proofs for complex theorems.

In short: The authors used a mix of deep number theory and a super-smart AI to prove that the "Hard Window" of obtuse triangles is almost entirely empty of the special "Lattice" variety. The treasure hunt is over; the room is empty.

Technical Summary

1. Problem Statement and Context

The paper addresses the Lattice Triangle Problem, a central question in the dynamics of rational billiards and the theory of translation surfaces.

• Rational Triangles: A triangle $T$ with interior angles $(\frac{p\pi}{n}, \frac{q\pi}{n}, \frac{r\pi}{n})$ where $p,q,r,n \in \mathbb{Z}_{>0}$ and $p+q+r=n$.
• Unfolding: Such a triangle unfolds into a translation surface $(X_T, \omega_T)$.
• Lattice Property: The triangle is a "lattice triangle" if the resulting surface is a Veech surface (its affine automorphism group is a lattice in $SL_2(\mathbb{R})$). This implies the $SL_2(\mathbb{R})$-orbit is closed, projecting to a Teichmüller curve.
• The Challenge: While acute and right-angled lattice triangles are fully classified, the classification of obtuse scalene triangles remains open.
• The "Hard Window": The most difficult regime involves obtuse triangles where the largest angle lies in the interval $(\pi/2, 2\pi/3]$. It is conjectured that no new lattice triangles exist in this window beyond two known infinite families and one sporadic example (Hooper's triangle).

2. Methodology

The authors employ a multi-faceted approach combining geometric obstruction theory, analytic number theory, and formal verification.

A. Geometric to Arithmetic Translation

The paper utilizes the Mirzakhani-Wright rank obstruction, a geometric criterion that restricts the possible affine invariant submanifolds of a lattice surface.

• Larsen-Norton-Zykoski Reformulation: The authors rely on a number-theoretic reformulation of this obstruction. A rational obtuse triangle is not a lattice triangle if there exists a "usable" unit $a \in (\mathbb{Z}/n\mathbb{Z})^\times$ such that at least two of the following modular inequalities hold:
  $$[ap]_n < [2p]_n, \quad [aq]_n < [2q]_n, \quad [ar]_n < [2r]_n$$
  where $[x]_n$ denotes the least non-negative residue.

B. Analytic Framework (Fourier Analysis)

To prove that such a unit $a$ exists for "almost all" triangles, the authors define a counting function $S(p, q)$ representing the number of units $a$ satisfying the first two inequalities simultaneously:
$$S(p, q) = \sum_{a \in (\mathbb{Z}/n\mathbb{Z})^\times} \mathbf{1}_{I_{2p-1}}(ap) \cdot \mathbf{1}_{I_{2q-1}}(aq)$$
The goal is to show $S(p, q) \geq 5$ (ensuring at least one usable unit exists).

• Decomposition: $S(p, q)$ is decomposed into a Main Term $M(p, q)$ and an Error Term $E(p, q)$ using discrete Fourier analysis and Ramanujan sums ($c_n(t)$).
  $$S(p, q) = M(p, q) + E(p, q)$$
• Main Term: $M(p, q) \approx \frac{(2p-1)(2q-1)}{n^2}\phi(n)$.
• Error Term: The challenge lies in bounding $E(p, q)$. A crude bound is insufficient.

C. The Role of Large Prime Factors

The core technical innovation is exploiting the arithmetic structure of the denominator $n$.

• Hypothesis: The authors focus on integers $n$ possessing a large prime factor $P = P^+(n)$ (specifically $P \geq n^{1/\log \log n}$).
• Cancellation Mechanism: Using properties of Ramanujan sums at prime powers (Lemma 3.2), they show that if $n$ has a large prime factor $P$, the Ramanujan sums $c_n(kp+\ell q)$ vanish for most frequencies unless specific congruence conditions are met.
• Exceptional Sets: They prove that for a fixed $q$, the error term is small for all $p$ except for a set of residue classes modulo $P^\alpha$ (where $P^\alpha || n$) that has density $\ll 1/P$.

D. Formal Verification

A significant portion of the paper documents the use of AxiomProver, an autonomous AI system, to formalize the proof in Lean 4.

• The AI was tasked with formalizing the analytic number theory estimates (specifically Theorem 6.1 in the draft).
• The system successfully corrected minor errors in the human draft and generated a complete, machine-verifiable proof in Lean.
• The human authors then optimized the proof to remove auxiliary parameters introduced by the AI, resulting in the final Theorem 1.1.

3. Key Results

Theorem 1.1 (Main Theorem)

Let $\Omega_+$ be the set of integers $n$ such that their largest prime factor $P^+(n) \geq n^{1/\log \log n}$. This set has natural density 1.
For $n \in \Omega_+$, let $L_n$ be the set of pairs $(p, q)$ in the obtuse region $H_n$ corresponding to lattice triangles. Then:
$$\lim_{\substack{n \to \infty \\ n \in \Omega_+}} \frac{\#L_n}{\#H_n} = 0$$
Interpretation: For a set of denominators of density 1, the proportion of obtuse rational triangles that are lattice triangles tends to zero.

Corollary 1.2

The proportion of lattice triangles in the "hard window" (obtuse scalene regime) tends to 0 along a density 1 subset of denominators. This provides strong quantitative evidence for the conjecture that the known list of obtuse lattice triangles is complete.

4. Significance and Contributions

1. Resolution of the "Hard Window": While previous work (Larsen, Norton, Zykoski) ruled out lattice triangles in the "strongly obtuse" regime (angle $> 2\pi/3$), this paper breaks through the "hard window" $(\pi/2, 2\pi/3]$, showing that lattice triangles are extremely rare (density 0) in this region.
2. Quantitative Density Result: The paper moves beyond qualitative "non-existence" to a quantitative statement, proving that the set of potential counter-examples has density 0.
3. Methodological Advancement: The paper demonstrates the power of combining Mirzakhani-Wright rank obstruction with analytic number theory (specifically the distribution of large prime factors and Ramanujan sums) to solve dynamical systems problems.
4. AI in Mathematical Research: This work serves as a landmark test case for AxiomProver. It demonstrates that AI systems can not only formalize complex proofs but also identify and correct subtle errors in human drafts, acting as a collaborative partner in high-level mathematical research. The successful formalization of the "main engine" (Theorem 6.1) in Lean provides a rigorous foundation for the results.

5. Conclusion

The paper effectively proves that the Mirzakhani-Wright rank obstruction is sufficient to disqualify almost all obtuse rational triangles in the hardest remaining regime. By showing that the existence of a large prime factor in the denominator forces the necessary arithmetic obstructions to hold, the authors confirm the "paucity" of lattice triangles, bringing the classification problem significantly closer to a complete solution. The integration of autonomous formal verification highlights a new paradigm for ensuring the correctness of complex analytic proofs.