Osprey rechecks imported mathematical proofs: for mathematicians
See actual imported mathematical proofs being checked by Osprey, with each theorem's assumptions made visible.
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 films record an earlier selection of supporting lemmas; the dated progress guide records the current public corpus separately. These are checked exports from Lean developments, not a completed port of Mathlib or the headline research theorems.
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
- Mathlib is Lean's community library of formalized mathematics: definitions, theorems, and proofs that later work can reuse. Osprey's port is underway. Its kernel is written in Osprey, and it rechecks imported Lean proofs. An actual Mathlib module is now in the importer.
- Lean provides a reference for developing Osprey's compatible theory. Osprey checks the imported evidence itself. Known soundness bugs must be rejected. The discipline protocol keeps theories separate; safe versioned forks and fresh proof checks remain required milestones.
- The fixture records output from Lean and its exporter, with the toolchain identity. Names, universe levels, terms, and declarations are serialized as text. Osprey reconstructs that environment and checks the supported declarations. The exact fixture is preserved so the demonstration can be repeated.
- The executable accepts and_swap, eq_symm, and iff_refl from the recorded export. In familiar notation, these express conjunction commutativity, equality symmetry, and self-equivalence. The checker has processed the proof terms and their declarations. These acceptance results concern this recorded set of theorems.
- Here is Lean's actual Nat.add_comm proof, imported and checked by Osprey. It says that natural-number addition is commutative. The check uses natural-number definitions and dependent elimination rules. Its recorded dependency closure contains no axioms. This is a universal theorem, not a numerical spot check.
- This imported loop lemma states an exact counter invariant: for every natural-number width, the returned work count is three times the width, plus one. This is an abstract counter, not a timing measurement. The Workbench reports the checked statement and its transitive assumption, propositional extensionality. The manifest pins the original statement and dependency export.
- The second result substitutes a term that does not have the arithmetic theorem's required type. The same executable rejects that declaration. This controls one concrete failure path. It strengthens evidence about the importer and kernel without claiming that their implementation has been proved correct.
- The selected corpus replays under all three backends. We are importing Euclid's theorem that there are infinitely many primes. Lean accepts the reference, and Osprey reads the exported proof. Long chains of definitions slowed the full check. A smaller dependency now checks under ARC. The guide records this progress and the remaining work.