The mathematics section now ships a full formalization plan: wiki/research/math/LEAN_PLAN.md (per-theorem Lean statement sketches, Mathlib dependencies, 3 difficulty tiers, dependency DAG) over the theorem corpus wiki/research/math/frahan_algorithm_derivations.pdf (~33 named results). Two decidable instances are already machine-proved with Z3 (wiki/research/math/verification/verify_instances.py).
Task (Tier 1, the recommended starters): lake new frahan_proofs math, pin a Mathlib toolchain, and mechanize the Tier-1 combinatorial/induction results per the plan: Sutherland-Hodgman subset lemma, guillotine DP optimality, Lloyd/k-planes monotone termination, Imai-Iri fewest-links optimality, Hertel-Mehlhorn 4-approx. Convention: each .tex Theorem N becomes theorem tex_<label> with a docstring citing the label.
Done when: a frahan_proofs Lake project builds sorry-free for at least 3 Tier-1 theorems, CI'able with lake build. Size: L (per theorem: S-M once the project skeleton exists).
The mathematics section now ships a full formalization plan: wiki/research/math/LEAN_PLAN.md (per-theorem Lean statement sketches, Mathlib dependencies, 3 difficulty tiers, dependency DAG) over the theorem corpus wiki/research/math/frahan_algorithm_derivations.pdf (~33 named results). Two decidable instances are already machine-proved with Z3 (wiki/research/math/verification/verify_instances.py).
Task (Tier 1, the recommended starters):
lake new frahan_proofs math, pin a Mathlib toolchain, and mechanize the Tier-1 combinatorial/induction results per the plan: Sutherland-Hodgman subset lemma, guillotine DP optimality, Lloyd/k-planes monotone termination, Imai-Iri fewest-links optimality, Hertel-Mehlhorn 4-approx. Convention: each .tex Theorem N becomestheorem tex_<label>with a docstring citing the label.Done when: a frahan_proofs Lake project builds sorry-free for at least 3 Tier-1 theorems, CI'able with
lake build. Size: L (per theorem: S-M once the project skeleton exists).