Welcome to The Incredible Proof Machine! This tool performs proofs in various logics (e.g. propositional, predicate logic) visually: you simply add blocks representing proof steps, connect them properly, and if the conclusion turns green, you have created a complete proof. Drag and drop to connect dots; for examples, see the paper. For a quick UI introduction, check the introductory video on the Tea Leaves Programming channel (13min)!

The Incredible Proof Machine was created to convey the fun and joy of doing proofs, especially computer-aided, without first learning the syntax of a "real" theorem prover like Isabelle. Keyboard shortcuts include CTRL+Z (Undo), CTRL+Y (Redo), CTRL+A (Select all), BACKSPACE/DELETE (Delete), SHIFT+MOUSE1 (Add to selection).

If the conclusion isn't green, your proof isn't complete: unconnected inputs (red), mismatched connections (red), cycles (red), or miswired local hypotheses (red). Enter formulas using abbreviations: & for ∧, | for ∨, -> for →, ^ for ↑, ~ for ¬, ! for ∀, ? for ∃, False for ⊥. Create custom tasks with multiple assumptions/conclusions on separate lines. Select blocks with Shift to create custom blocks.

Currently proofs save only in browser local storage. Joachim Breitner created this with help from colleagues. Publications include ITP 2016 paper, LFMTP 2016 invited talk, and Isabelle formalisation in Archive of Formal Proofs (May 2016). Everything is Free Software; contributions welcome.