The Lattice Triangle Problem in the Hard Obtuse Window
The lattice triangle problem asks which rational triangles unfold to Veech surfaces; in the hard obtuse window it is conjectured that none do. Via an arithmetic reformulation of the Mirzakhani-Wright rank obstruction, the paper rules out all but a density-0 subset of triangles in that window.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Teichmüller dynamics
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-03-25
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
A density-1 obstruction, not a full resolution: the conjecture that the hard window contains no lattice triangles remains open on a density-0 set.
What the AI did
"The main engine in this paper (Theorem 6.1) was autoformalized by AxiomProver in Lean (using mathlib)" - a test case for the autonomous system, with the protocol and artifacts documented in their own section.
Verification
The paper's main engine is autoformalized and kernel-checked in Lean by AxiomProver; the surrounding derivations are informal, and no independent review has appeared. Tier: the main engine was autoformalized by AxiomProver itself; the informal-to-formal correspondence is author-audited only.