lean-check

# Lean Check: Machine-Prove a Self-Authored Lemma Formalize a lemma/theorem in Lean 4 + mathlib and let the kernel check it. A `lake build` that succeeds **with no `sorry` and no extra axioms** is a machine-verified proof — the strongest guarantee available. ## When to Use - A **critical lemma** whose correctness you want beyond doubt (the load-bearing step of a theorem). - `lean-check`, "formalize this in Lean", "machine-check this lemma", "prove this in Lean 4". - After `numerical-check` fails to falsify a claim and it's important enough to *prove*. ## When NOT to Use | Situation | Use instead | |---|---| | Stress-test / hunt a counterexample to a distributional claim | `numerical-check` (R1) | | Verify an algebra / derivative / limit / closed-form step | `symbolic-check` (R2) | | A statement too rich to faithfully formalize in reasonable time (heavy measure theory, bespoke objects) | `domain-reviewer` — do NOT force a lossy Lean statement | ## Position in the verification spectrum **R3 — formal machine proof.** The top rung: `lake build` (clean, `sorry`-free) = a kernel-checked theorem. Cost is high (formalization effort + statement fidelity), so reserve it for the claims that matter most; use R1/R2 to triage first. ## Toolchain (pre-seeded — do not re-download) - **Machine:** Mac Mini (`[server]`). Check `hostname`; if on the MacBook, run via `ssh mini`. - **Project:** `~/lean-verify/mathlib_verify/` — Lean `4.31.0`, mathlib `v4.31.0` (cache-backed, ~7.2 GB `.lak...