Guided proof

Proof tutorial

Choose a lesson

Enter one tactic at a time. The kernel checks each line, and every proof state stays visible below.

Current theorem

Loading theorem…

0 tactics

Next tactic Press Enter to apply

Proof state history

Starting state

Preparing the first proof state…