proof's ladder had T0 propositional + T1 z3 real, but no proof-assistant
backend — the capability gap vs AlphaProof/Aristotle/Axiom, which all
build on Lean + Mathlib. Add LeanVerifier: a real Solver rung that runs
the `lean` typechecker on a goal whose statement IS a complete Lean
theorem-with-proof and reports what Lean actually decided:
- typechecks (exit 0, no error:, no sorry) -> Proved. Lean is THE verifier
that makes Proved meaningful — the trust root, not a model stand-in.
- `decide` reports the proposition false -> Refuted, carrying Lean's
message as the counter-model witness (a decision; the cascade halts and
never escalates a disproof).
- other failure, or `lean` absent -> Unproved (this rung didn't close it).
available() lets a builder skip the rung when the toolchain is missing.
Goal->Lean encoding is the caller's (context names the dialect); only
Lean-dialect goals are attempted. Energy is ModelBased (wall time x the
crate's power model), like the z3 rung.
Validated END-TO-END against a real lean 4.31.0: 1+1=2 by decide -> Proved,
1+1=3 by decide -> Refuted, 2+2=5 := rfl -> Unproved, `sorry` -> not
proved, an SMT goal -> skipped. clippy clean. No new deps (std::process).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
77e8456460