Inside a small proof kernel: for mathematicians

Follow a statement and its evidence through the proof kernel written in Osprey.

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

The kernel infers a proof term's type and compares it with the claimed statement. The recorded runs show both acceptance and deliberate rejection. This is a check of the supplied statement and proof, not automatic verification of an entire application.

Read the guide and try it yourself. Osprey is actively evolving; the guide distinguishes the recorded demonstration from current corpus progress.

Actual source

• examples/proof/kernel/src/infer.ospml
• examples/proof/kernel/src/checked.ospml

Continue learning

Use the Workbench · Current Mathlib port evidence · All twelve films

Transcript

1. 0:00 A proof kernel checks whether a formal proof term has the type representing its theorem. Osprey is a functional programming language with a kernel written in Osprey. We will follow a dependent function example through inference, reduction, and comparison, explaining each step as it appears.
2. 0:19 Terms are tagged values. A sort gives a type of types at a universe level. A variable refers to a binder, a named input. A function type records its input and result. Application supplies an argument.
3. 0:34 Inference computes a term's type. Reduction simplifies terms by computation. Two terms are definitionally equal when they reduce to the same normal form. The checker compares normal forms structurally, including every binder and universe argument. A difference is an error.
4. 0:52 The surface parser reads declarations like the identity theorem and a chained implication. An elaborator turns each into a kernel term. Identity and typed implication composition check. A declaration claiming q from only p is rejected. The elaborator invents no unknown terms.
5. 1:13 The run prints the accepted identity and the rejected variant. The kernel's reason names the terms that failed to match. Nothing is waved through because a theorem has a promising name. The rejection controls the acceptance.
6. 1:28 Ordinary Osprey retains Hindley-Milner inference. A generic compile-time protocol delegates additional disciplines to packages; the existing interval-bound checker demonstrates another discipline. The dependent-proof kernel also lives outside the compiler. Here it accepts universal addition commutativity. Versioned theory forks, explicit axiom policies and invalidation of dependent proof receipts remain completion milestones. Changing a discipline must never preserve incompatible proof authority.