Proofs and mathematics in Osprey

A proof states a precise claim and supplies evidence a checker can verify. Osprey has a proof kernel written in Osprey, a Workbench for building small arguments, and an ongoing library port that already checks real exported mathematical proofs.

Lean as an oracle

Lean supplies reference statements, proof certificates and executed checks while Osprey develops its own proof technology. Osprey's kernel makes its own decisions; source authoring, automation and library reconstruction have separate completion milestones. The goal is independent operation with replaceable disciplines and room for further capabilities.

An oracle can contain implementation defects. Known unsound certificates must be rejected even if an affected Lean release accepts them. A corrected checker, changed axiom policy or forked theory needs its own identity and fresh validation of dependent proofs; previous Checked badges cannot simply carry over. This does not assert that Lean's underlying mathematical theory is inconsistent.

The current evidence guide distinguishes delivered results from remaining work. The completion milestones specify the source frontend, automation, full library and independent-operation gates.

Choose your starting point

For programmers: start with dependent types, then use the Workbench. No calculus or prior proof-assistant experience is assumed. For mathematicians: choose the mathematics versions for terms, goals, assumptions and the import boundary. Both paths use real Osprey code and applications.

Each film runs about two to three minutes, with English captions, seekable chapters and a full transcript. Watch in this order, or choose a topic below.

Try the tools

• Proof Workbench guide: open the app, follow the first proof, inspect goals and use guided lessons.
• Mathlib port: current evidence: reproduce the checked imports and understand which claims remain open.
• Dependent types and proofs specification: the full intended contract, distinguished from delivered results.

What are dependent types?

Types can describe facts about values. Start with a list-length example, then watch Osprey check an actual identity proof.

For programmers · For mathematicians

For programmers

For mathematicians

The length-indexed list is a conceptual introduction, not a shipped Osprey API. Ordinary Osprey programs retain Hindley-Milner type inference; dependent proof terms belong to a separate checking discipline.

How Osprey checks a proof

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

For programmers · For mathematicians

For programmers

For mathematicians

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.

Use the Proof Workbench

Write a small argument, inspect hypotheses and goals, and complete a guided exercise in the real Workbench.

For programmers · For mathematicians

For programmers

For mathematicians

A Checked verdict comes from the shared Osprey kernel. A draft can still contain open goals, and unsupported or mismatched steps must be refused. The optional generated source is a separate view; its presence alone does not establish a proof. The films show the layout recorded during production, including some freehand board controls. The supported proof workflow uses typed formulas and proof steps; these videos do not demonstrate mathematical handwriting recognition.

The Mathlib port is underway

See actual imported mathematical proofs being checked by Osprey, with each theorem's assumptions made visible.

For programmers · For mathematicians

For programmers

For mathematicians

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.

A proof checker must say no

Compare a valid proof with deliberately corrupted evidence and a false replacement statement.

For programmers · For mathematicians

For programmers

For mathematicians

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.

Navier-Stokes: the solution and Osprey

Learn what OpenAI solved, inspect the fluid equations in the Workbench, and explore computation and checked reasoning in Osprey.

For programmers · For mathematicians

For programmers

For mathematicians

On 8 September 2026, OpenAI published a solution with a Lean formalization: smooth forcing produces a finite-time singularity from initially smooth fluid at rest while energy remains finite. The films explain that result before exploring Osprey. The periodic two-dimensional Taylor-Green flow is a separate numerical example with measured residuals; the Workbench exercise checks a propositional implication under explicit premises. Separately, Osprey checks selected computability, work-counter and number-theory exports from openai/math, while the complete headline theorem remains to be ported. The recorded computation and residual checker are production assets in the separate TikTok repository; the source link below opens the Workbench lesson.

The flow demonstration supplies numerical evidence; it does not claim a formal Navier-Stokes proof. The published OpenAI solution is a separate result: an internal system's analytical proof, formalized in Lean, that a smooth fluid initially at rest under a smooth force develops a finite-time singularity while its energy stays finite (source). Separately, Osprey checks seventeen selected lemmas about stacks, loop work, finite indices and number theory from pinned openai/math sources, not the headline Navier–Stokes proof. The imported corpus is a working step toward Mathlib, not the whole library. Osprey is actively evolving.