lean-check

name	lean-check
description	Use when you need to MACHINE-CHECK a self-authored lemma/theorem by formalizing it in Lean 4 + mathlib and running `lake build` — the strongest verification (a clean build with no `sorry` IS a proof). R3 of the verification spectrum. Runs against the pre-seeded mathlib project at ~/lean-verify/mathlib_verify on the Mac Mini. Triggers: /lean-check, 'formalize this lemma in Lean', 'machine-check this theorem', 'prove this in Lean'. NOT for stress-testing a distributional claim (use /numerical-check), an algebra step (use /symbolic-check), or claims too rich to faithfully state (escalate to domain-reviewer). The hard part is a FAITHFUL statement — a Lean lemma that doesn't match the paper is false confidence.
allowed-tools	["Read","Write","Edit","Bash","AskUserQuestion"]

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 .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.

5. Emit the verification report + keep the .lean

Verdict semantics (important)

Outcome	Verdict
Faithful statement, clean build, no sorry, standard axioms only	VERIFIED
Proved the negation	FALSIFIED
Faithful statement, proof didn't close after real effort	INCONCLUSIVE (unproven)
Can't faithfully formalize the claim	INCONCLUSIVE (not formalizable)
Toolchain / build-system failure	ERROR

Anti-Patterns

• Don't trust a green build without checking sorry/admit and #print axioms — a sorry builds fine and proves nothing.
• Don't weaken/alter the statement to make it build — the statement is the claim; a proof of a different statement is false confidence.
• Don't read "proof didn't close" as FALSIFIED — inability to prove ≠ disproof.
• Don't force a rich probabilistic/measure-theoretic claim into a lossy Lean proxy — report not-formalizable and escalate to domain-reviewer.
• Don't write into paper-{venue}/paper/ or re-scaffold mathlib — use the seeded project scratch.
• Don't run bare python/toolchain guesses — Lean via lake only.

Output — Verification Report (shared *-check shape)

Write to reviews/<scope>/verify-lean/<YYYY-MM-DD-HHMM>.md, and copy the .lean module beside it (or note its path):

claim:    <informal statement> ⟶ <Lean statement (verbatim)>
fidelity: <one line: why the Lean statement faithfully encodes the claim>
method:   R3 Lean 4 (v4.31.0) + mathlib; lake build; sorry-free; axioms = <#print axioms output>
verdict:  VERIFIED | FALSIFIED | INCONCLUSIVE (unproven|not formalizable) | ERROR
reproduce: cd ~/lean-verify/mathlib_verify && lake build MathlibVerify.<Name>   (module attached)

Verification (did this skill work?)

• lake build MathlibVerify.<Name> exits 0.
• grep sorry is empty AND #print axioms shows only the standard three.
• The ## fidelity line exists — no VERIFIED without an explicit statement-faithfulness argument.

Worked example (toolchain smoke)

theorem lc_smoke (a b : ℝ) (h : a ≤ b) : a - 1 < b + 1 := by linarith → lake build exit 0, no sorry, standard axioms → VERIFIED. (A faithful Lean formalization of the median-collapse theorem itself — Φ, medians of distributions, the large-council limit — is a genuine formalization project; /lean-check is for the tractable load-bearing lemmas, with R1/R2 covering the rest.)