Formal Math Lean Proof Witness
Compiles a tiny Lean example with the real prover and records whether it built, leaking no proof text.
Contract
Does This takes a small, purpose-built Lean math file (a handful of toy theorems written just for this demo) and a tiny project setup, copies them into a throwaway scratch folder, and actually tries to compile them with the installed Lean theorem-prover and its Lake build tool. It then writes down exactly what happened: whether the Lean and Lake tools were found, whether the build passed, fingerprints (hashes) of the source files, the names of the theorems it defined, and how many lines each file had. It also deliberately feeds in a broken proof and a couple of off-limits files to confirm they get rejected. The point is to show real proof-checking machinery run on a small example, while keeping the written records honest and redacted: no proof text or internal logs leak out, and it states plainly that this is a narrow toy check on one fixture, not a general-purpose proof system.
Scope limit It authorizes only a witness that a tiny declared public toy proof compiled under the locally installed Lean/Lake toolchain in a temporary workspace, plus confirmation that its leakage guardrails fired. It excludes Mathlib/Aesop/Batteries-dependent or general proof or theorem-program authority, external model access, private proof import, benchmark or performance claims, whole-system correctness, or any launch, hosted deployment, or public sharing.
Run
PYTHONPATH=src python3 -m microcosm_core.organs.formal_math_lean_proof_witness run --input fixtures/first_wave/formal_math_lean_proof_witness/input --out receipts/first_wave/formal_math_lean_proof_witnessEvidence
ClassExternal tool runevidence 4/5Real runtime resultRuns real tools
Links to Formal Math Premise Retrieval, Formal Math Readiness Gate, Proof Diagnostic Evidence Spine, Verifier Lab Kernel, Verifier Lab Execution Spine