A proof checker must say no: for programmers
Compare a valid proof with deliberately corrupted evidence and a false replacement statement.
For programmers. Choose the other audience version or browse the complete series.
Lean is the development oracle for compatible proofs; Osprey checks them independently. Known unsound reference behaviour must be refused, and changing a discipline requires fresh proof validation.
What this demonstrates
A trustworthy check needs negative controls. Acceptance must disappear when the evidence or statement changes; a parser error or missing dependency is not a substitute for a kernel type-mismatch rejection.
Read the guide and try it yourself. Osprey is actively evolving; the guide distinguishes the recorded demonstration from current corpus progress.
Actual source
Continue learning
Use the Workbench · Current Mathlib port evidence · All twelve films
Transcript
- A proof checker should accept valid evidence and refuse invalid evidence. Both results matter. Osprey is a functional programming language, and its proof checker is written in Osprey. We will run a valid example beside a deliberately wrong one and read the explanation.
- This function receives evidence for p and claims to produce evidence for q. Returning the same value does not turn one claim into the other. The mismatch is exactly what the checker should catch. A convincing theorem name cannot repair a bad proof term.
- The checker does not compare pretty printed words. It compares structured terms. Names can be reused in different places, so each name must point to the right input. Constants also carry information the checker needs. Structure keeps those differences visible.
- The same rule applies when reading another system's export. If the reader meets a form it does not support, it reports that form. It must not skip the declaration and still report success. Refusing is safer than pretending to check.
- A checked theorem still sits inside a trust boundary. You need the exact statement, its assumptions, the proof term, and the checker that accepted it. Tests strengthen the checker, but a passing suite is not proof that it has no bugs.
- Keep the valid and invalid cases together. Check that identity passes, then inspect the wrong term and its rejection. That habit makes proof tools easier to trust: state the claim, show the evidence, and show the limits too. Osprey is actively evolving.