Natural deduction and Lean

Construct a derivation and translate it to Lean, or enter a Lean proof to reconstruct its natural deduction tree.

Scope. The book’s teaching fragment: intro, apply, exact, and constructor terms; the first-order translator also supports typed have subproofs, quantifiers, rfl, and Eq.subst. General elaboration and Mathlib require Lean.

Propositional proofs

Use one variable (... : Prop) declaration and one example per translation.

First-order proofs

Declare Domain : Type and the objects, predicates, and functions you use. Use one example per translation.

Using it

Select a derivation’s conclusion and choose the down arrow (ND → Lean). Enter a completed Lean proof and choose the up arrow (Lean → ND) to check and draw its derivation. The external Open in Lean link opens the current code in the playground for kernel checking.

Goals lets you work backwards. Exporting an unfinished plan puts sorry at open goals; complete those proofs before importing the code again. The canvas also supports proof downloads, saved lemmas, and LaTeX export.

In the book

• Chapter 7 · Lean introduces the proof constructions.
• Chapter 7 · Curry–Howard correspondence relates proofs to typed terms.
• Chapter 9 · First-order proofs in Lean introduces object types, predicates, and quantifiers.