The proof workbench: goals and evidence: for mathematicians
Write a small argument, inspect hypotheses and goals, and complete a guided exercise in the real Workbench.
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 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 state records the assumptions available to you and the goal you must establish. Osprey is a functional programming language, and its proof workbench makes that state visible while you write. We will follow a conjunction proof and then explore a lesson.
- Statement: if p and q both hold, then q and p both hold. Assume the pair. By cases introduces its two parts as hypotheses. Next, split the required conclusion into q and p, and supply their evidence in that order. Each move must follow a rule the checker accepts.
- The goal pane shows a context and a conclusion. The context lists hypotheses you have assumed. The conclusion is what remains to prove. A hypothesis named p is not a proof of every claim about p. Read both sides before choosing a step.
- Open Examples to find lessons and challenges. Read the explanation, attempt the exercise, and submit your answer. Hints are available. After three incorrect proof submissions, Show solution reveals a worked proof. Study and submit it to the kernel, then inspect the feedback.
- Source shows the theorem text generated from your argument, with explicit holes for unfinished steps. This text did not produce the displayed verdict: Osprey's own kernel checked your steps directly. Passing the generated file to Lean is a separate path that is still being built.
- For a first session, complete And, the other way around. Then swap its last two steps and read the kernel's reason for refusing it. A proof of p cannot discharge the goal q. The changing proof state explains the result. Osprey is actively evolving.