A self-contained, machine-checked formalization of the three-gap theorem (also called the three-distance theorem, or Steinhaus's conjecture) in Lean 4 on top of Mathlib.
Theorem. For every real number
aand everyN ∈ ℕ, the points{ i·a mod 1 : 0 ≤ i < N }partition the half-open interval[0,1)into gaps taking at most three distinct lengths; and when exactly three lengths occur, the largest is the sum of the other two.
The two formalized statements live in ThreeGap.lean:
| Statement | Lean declaration |
|---|---|
| At most three distinct gap lengths | ThreeGap.three_gap_card_le_three |
The three lengths are η⁺, η⁻, η⁺+η⁻ (largest = sum of the others) |
ThreeGap.three_gap_lengths_eq |
Both are proved with no sorry and depend only on the three foundational
axioms propext, Classical.choice, Quot.sound that underlie Mathlib itself.
- Uniform in the rotation number. The same proof covers rational and
irrational
a, with no case split. The only previous formalization (Mayero's Coq development after van Ravenstein) is restricted to irrationala. To our knowledge this is the first formalization of the theorem in Lean 4. - First-return route. The proof works in
[0,1)viaInt.fract(notAddCircle), through the two return timesη⁺,η⁻. The hard "corner" case—that the longest gap is empty—is closed by a self-contained return-time/period argument that removes the irrationality restriction.
This is not a new mathematical proof of the theorem; elementary proofs valid
for all a are classical (e.g. Liang's 1979 rigid-gap argument). The
contribution is the machine-checked formalization. See the companion paper for
the full discussion of prior work.
A companion article describing the formalization is in
paper/three_gap_theorem_lean.tex:
A Lean 4 Formalization of the Three-Gap (Steinhaus) Theorem, Uniform in the
Rotation Number. Build it with latexmk -pdf three_gap_theorem_lean.tex.
Requires the Lean 4 toolchain
(elan), which picks up the pinned versions automatically:
- Lean:
leanprover/lean4:v4.29.1(pinned inlean-toolchain). - Mathlib:
v4.29.1, exact commit5e932f97dd25535344f80f9dd8da3aab83df0fe6(pinned inlake-manifest.json).
# fetch the prebuilt Mathlib cache (recommended; avoids recompiling Mathlib)
lake exe cache get
# build the module
lake buildTo inspect the trust base yourself, add to the end of ThreeGap.lean:
#print axioms ThreeGap.three_gap_card_le_three
-- 'ThreeGap.three_gap_card_le_three' depends on axioms:
-- [propext, Classical.choice, Quot.sound]and there is no sorry in the file:
grep -c 'sorry' ThreeGap.lean # 2 matches — both inside comments onlyThe orbit { i·a mod 1 : i < N } is, for rational a, the same kind of
projected point set as those produced by the one-dimensional rational
cut-and-project construction of the companion project (the precise
correspondence involves a change of rotation number; see the paragraph
"Relation to the companion work" in Section 7 of this repository's paper). Its gap sequence and minimal period (under both the multiset
and set conventions) are studied there:
https://github.com/dkunert/cut-and-project.
The Lean formalization, the proof strategy, and a first draft of the companion paper were produced by Anthropic's Claude (Claude Opus 4.8) through the Claude Code agent, under the author's direction and coaching. The author has independently verified the mathematical content and accepts full responsibility for the results and any errors. The correctness of the results rests not on this provenance but on the Lean 4 kernel: anyone can rebuild the module and inspect the axiom list above.
MIT — see LICENSE. © 2026 Dirk Kunert.