Build notes

Lean is the active formalization path. Isabelle is a comparison base (vendored AFP) and is not required on the development box.

Lean

Toolchain lockstep with other tangentproofs repos: leanprover/lean4:v4.35.0-rc1, Mathlib pin 09a9e06e4e5ccd5b783f25e52ad3ebecfb1e2d68.

cd lean
lake exe cache get   # never build Mathlib from scratch
lake build

List paper-facing theorems:

./scripts/list-results.sh
# or: (cd lean && ./scripts/list-results.sh)

Always run lake exe cache get before lake build. Building Mathlib from source can take hours.

Isabelle (comparison base)

Lean is the active formalization path. Isabelle is a comparison base (vendored AFP). This shared box has Isabelle2025-2 at /home/box/Isabelle2025-2 (isabelle on PATH via /home/box/bin/isabelle). The vendored session machine-checks green here (Memnar #1535).

Install Isabelle (this box: Isabelle2025-2; AFP entry targets HOL-Analysis).
Optionally install a matching AFP release, or use the vendored tree alone (session depends only on HOL-Analysis).

From isabelle/:

isabelle build -d afp-Euler_Polyhedron_Formula -v -o document=false Euler_Polyhedron_Formula

Expected: session Euler_Polyhedron_Formula builds from Euler_Formula.thy (ROOT timeout option is 300s). Document generation under document/ is optional. First build of HOL-Analysis may take ~10 min wall time; then the AFP session is ~15 s.

Status

AFP vendored as comparison base (afp-Euler_Polyhedron_Formula/).
Isabelle2025-2 installed on this box; vendored session machine-checks green (Memnar #1535).
Poly100 kept as historical archive.
Lean under lean/ is the active path (lake build).