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

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 .lake). Health check: cd ~/lean-verify/mathlib_verify && lake build MathlibVerify.SmokeTest.
• Refresh mathlib later: lake update && lake exe cache get.

Procedure

1. State the lemma FAITHFULLY (the hard part — get this right or the check is worthless)

• Write the Lean statement so it provably matches the informal claim. A too-weak, too-strong, or subtly-different statement that happens to build gives false confidence — the single worst failure mode.
• Before proving, read the Lean statement back against the paper's exact hypotheses and conclusion. State every hypothesis (domains, 0 < ρ < 1, StrictMono, etc.). When unsure the encoding is faithful, ask the user to confirm the statement.
• If the object cannot be faithfully stated in available mathlib (e.g. a bespoke distributional limit), STOP — report INCONCLUSIVE (not faithfully formalizable); do not ship a lossy proxy.

2. Write the module into the mathlib project scratch (NEVER the Overleaf paper)

Write to ~/lean-verify/mathlib_verify/MathlibVerify/<Name>.lean:

import Mathlib
theorem <name> (<hyps>) : <conclusion> := by
  <tactic proof>

3. Prove with mathlib tactics; iterate

• Try: simp, norm_num, ring, linarith/nlinarith, positivity, gcongr, field_simp, exact?, apply?, polyrith.
• Iterate on the proof, not the statement. If you find yourself weakening the statement to make it build, STOP — that's cheating the check.

4. Build and read the verdict

cd ~/lean-verify/mathlib_verify && lake build MathlibVerify.<Name>

• Exit 0 + no sorry → candidate VERIFIED. Confirm no shortcuts:
  • grep -n 'sorry\|admit' MathlibVerify/<Name>.lean → must be empty.
  • Add #print axioms <name> and rebuild → must show only propext, Classical.choice, Quot.sound (mathlib's standard axioms); sorryAx present ⇒ NOT proven.
• Statement doesn't typecheck → formalization error (fix the statement, re-verify fidelity).
• Builds but proof won't close after honest effort → INCONCLUSIVE (unproven; claim may still be true). Failing to prove is NOT a disproof.
• You prove the negation (¬ <claim>) → FALSIFIED.