Meet the proof workbench: for programmers
Write a small argument, inspect hypotheses and goals, and complete a guided exercise in the real Workbench.
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 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.
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 workbench helps you write an argument and see what remains to establish. Osprey is a functional programming language, and its workbench is an Osprey application. Let’s write a small proof, inspect its goals, and try a tutorial.
- Start with a small statement. If both p and q are true, then q and p are true. Assume the pair, then take it apart into the two facts. Ask for q first, then p. Watch the pane after each step: sometimes your available facts change, and sometimes the remaining goals do.
- The goal pane is the important part. It lists the facts you have assumed and the claim you still need to prove. A useful name is not enough: the fact it names must match the goal. If a step does not fit, read the goal before changing the argument.
- Open Examples to find short lessons and challenges. Read the explanation, try the exercise, then submit your answer for checking. A hint can unblock you. After three incorrect proof attempts, Show solution reveals a worked answer. Study it, then submit it to see the kernel check the proof.
- Open Source to see a text version of your argument. Unfinished parts appear as explicit holes. The verdict comes from Osprey's own kernel checking your steps directly. Sending this generated file to Lean, another proof assistant, is a separate path that is still being built.
- For a first session, try And, the other way around. Then swap its last two steps. The first asks for q, but you give it p. Watch the checker refuse that argument and read why. You can see what the rule requires. Osprey is actively evolving.