Freek #13 · tangentproofs

Euler's Gem

Lean 4 (+ archived Isabelle) formalization of Euler's polyhedron formula and the Euler–Poincaré characteristic for convex polytopes (popularized in David Richeson's Euler's Gem).

Browsable Results.lean

Syntax-highlighted, cross-linked Lean sources — start at the paper-facing results; identifier links fall through to Mathlib docs.

Lean ↔ AFP map

Cross-reference between Results.lean theorems and Paulson's AFP entry.

Build notes

Lean (lake) and Isabelle recipes. Isabelle2025-2 is installed on this box; vendored AFP session checks green.

Source on GitHub

Active Lean under lean/; vendored AFP under isabelle/.

What's proved (Lean)

Paper-facing claims from lean/Results.lean — only what is actually proved.

Theorem	Meaning
`results_euler_characteristic`	Euler characteristic of a full-dimensional convex polytope is `1`
`results_euler_relation_dimension_three`	Euler's formula: in dimension 3, `V − E + F = 2`, proved from that characteristic
`results_picks_theorem`	Pick's theorem: area `= I + B/2 − 1` for a strictly convex lattice polygon
`results_five_platonic_solids`	Euler's formula leaves five Platonic solids: tetrahedron `{3,3}`, cube `{4,3}`, octahedron `{3,4}`, dodecahedron `{5,3}`, icosahedron `{3,5}`
`results_pick_count_of_euler`	Euler's formula for a triangulation gives Pick's count `I + B/2 − 1`
`results_fan_pick_of_euler`	An empty fan's Pick count follows from the Euler characteristic
`results_disk_pick_of_euler`	A triangulated disk's Pick count follows from the characteristic, by moves that preserve `V − E + F`

Strategy

Lean (primary): follow Lawrence C. Paulson's AFP Euler's Polyhedron Formula (2023; HOL Light port, credited to Jim Lawrence) — hyperplane arrangements + cell complexes + Euler-characteristic invariance. Target: Euler–Poincaré for full-dimensional convex polytopes, then V − E + F = 2 in dimension 3.

Isabelle (comparison base): the same AFP entry is vendored under isabelle/afp-Euler_Polyhedron_Formula/. See the Lean ↔ AFP map. Do not invent a fresh Isabelle development.

Historical: isabelle/Poly100.thy is an earlier unfinished Isabelle attempt (Tverberg triangulation) predating the AFP entry — kept for provenance only.

Layout

lean/          Lean 4 project (active) — Lake / Mathlib / Results.lean
isabelle/      Vendored AFP Euler_Polyhedron_Formula + Poly100 archive
scripts/       Comparator helpers (list Results.lean theorems)
site/          This documentation site (GitHub Pages)
docs/          Browsable Lean sources (built in CI from lean/)

Phase B (#1535)

Paper-facing: the Euler characteristic, V − E + F = 2 in dimension 3, Pick's theorem for a strictly convex lattice polygon, and the five Platonic solids (tetrahedron, cube, octahedron, dodecahedron, icosahedron).