Peano Lab

sound arithmetic proofs · no install · self-hosted
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:
research:

Paste a complete Peano Lab proof

Paste one command per line, beginning with pa prove … and ending with qed. Blank lines are ignored. Commands run in order and stop at the first failed line; the successful prefix remains available to inspect or undo.

Limit: 256 nonblank commands, 100,000 characters total, and 8,192 characters per command. Pasting never authorizes a file download.

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. Paste a complete multiline proof directly at an empty prompt or use paste multiline proof. script previews the current replay; type script download directly to save it. ↑/↓ history · TAB completion.