Formalize · guard · Lean 4 kernel · axiom audit

Proof Checker

A pipeline that takes a theorem written in prose, formalizes it into Lean 4, compiles it against the kernel, and then audits which axioms the result actually depends on. Below are recorded runs, replayed exactly as they happened — including the ones that failed.

Recorded runs
73
Verified
44
Rejected
6
Kernel
Lean 4
Library
Mathlib

replay of recorded runs — nothing is executed in your browser

Mechanism

What the checker actually does

The claim is not "an assistant thinks this proof is right". It is that a kernel accepted a formal statement, and that an audit enumerated every axiom the accepted proof rests on. Each stage can reject.

prose statement what you wrote formalize prose → Lean 4 guard does it still say that? Lean kernel lake env lean axiom audit #print axioms statement + proof statement fidelity every step what it rests on diagnose & repair or stop and say why drifted won't compile extra axiom
The guard is the step that makes the rest meaningful: a formalization that quietly weakens the statement would compile perfectly and prove nothing. Rejection at any stage returns a diagnosis rather than a verdict — the fourth run below is a rejection whose diagnosis found a bug in the harness, not in the mathematics.
Recorded runs

Four runs, start to finish

Pick a run to see what went in, the Lean that came out, and what the kernel and the audit said about it.