starting…
GOALSThe focused obligation comes first; every remaining goal must also be closed.
CONTEXTVariables and hypotheses available to the focused goal, newest first.
CERTIFICATETactics fill a proof term;
qed asks the independent kernel to check it.start:
prove:
The complete prover runs locally in a Web Worker, using a self-hosted Python runtime, so a long search never freezes this page and Stop can terminate it. Every executable asset is served from this site (no CDN), and commands are not sent elsewhere; a ?cmd= deep link is part of the URL and can appear in server logs. The tactic layer is never trusted: every qed checks the finished certificate against the original theorem in the small kernel. ↑/↓ history · TAB completion.