Rejection is part of the proof: for mathematicians
Compare a valid proof with deliberately corrupted evidence and a false replacement statement.
For mathematicians. 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 theorem checker must distinguish a term of the claimed type from an impostor. Osprey is a functional programming language with a proof kernel written in Osprey. We will compare accepted terms, type mismatches, and unsupported imports to make its current trust boundary concrete.
- This function receives a proof of p and claims to return q. Returning the same term does not change its type. The kernel should reject the mismatch, and it does. A theorem's name cannot repair an invalid term.
- The kernel compares structured terms, not rendered text. A variable refers to its binder, so two occurrences of the same name can mean different inputs. Constants carry universe arguments. Ignoring either distinction would accept invalid proofs. The tests target them.
- An import reader follows the same rule. If an expression form is unsupported, the reader must report it. It must not skip the declaration and announce success. The current reader reports them explicitly. That matters while its theory is smaller than Lean's.
- A checked theorem depends on: the exact statement, its assumptions, the proof term, and the kernel that accepted it. Testing can find bugs, but a green suite is not a theorem that the kernel is correct. State the boundary with the claim.
- Keep the valid and invalid cases together. Confirm identity passes, then inspect the rejected term and reason. A proof tool becomes easier to assess when its limits are as visible as its successes. Osprey is actively evolving.