On the paucity of lattice triangles

These files accompany the paper arXiv:2603.23928.

Input files

• .environment: lean version
• task.md: description of the task to be completed
• problem.tex: informal problem statement
• informal_proof.tex: draft of the proof by K.O. (which contained some correctable mistakes)

Output files (Run with Lean 4.26.0)

• LatticeTriangle/problem.lean: translation of the problem statement into formal language (Lean)
• LatticeTriangle/solution.lean: solution in formal language (Lean)

Verifying with Comparator

This repository can be verified against the formal problem statement with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:

lake env comparator comparator.json

License

This repository uses the MIT License. See LICENSE for details.

Repository maintainers

• Evan Chen
• Kenny Lau
• Ken Ono
• Jujian Zhang