The Incredible Proof Machine (2016)

The Incredible Proof Machine is a visual environment designed for constructing proofs in predicate and propositional logic. Rather than wrestling with complex text-based syntax, users simply arrange logic blocks and link them together. A proof is considered successful when the final conclusion turns green.

🛠️ How it Works

The core mechanic is a drag-and-drop interface. You connect dots between blocks to build your logical argument.

For those seeking a visual walkthrough, a 13-minute introductory guide is available on the Tea Leaves Programming YouTube channel. Additionally, completed proof examples can be found in the associated research paper.

⌨️ User Interface & Controls

The tool is designed to be intuitive, utilizing several keyboard shortcuts for efficiency:

Action	Shortcut
Undo	`CTRL + Z`
Redo	`CTRL + Y`
Select All	`CTRL + A`
Delete Selection	`BACKSPACE` or `DELETE`
Multi-select	`SHIFT + Mouse1`

❓ Troubleshooting: Why is my conclusion not green?

If your conclusion remains red, it is likely due to one of the following issues:

Dangling Inputs: One or more blocks have an assumption input that isn't connected to a source.
Logical Mismatches: You have connected two propositions that are fundamentally different. These are flagged in red with a $\☠$ symbol.
Ambiguity: The connection is underspecified, meaning the system cannot verify if the propositions are identical. These are flagged in red with a $?$ symbol.

Pro Tip: If you encounter an underspecified connection (the $?$ mark), you can resolve this by inserting an annotation block ( $\✎ P$ ).

🧠 Advanced Logic Concepts

Local Hypotheses

In this system, local hypotheses are represented by outputs located to the left of a "dent" in a block. These specific outputs are restricted; they can only be utilized within the section of the proof that connects to the corresponding input on the right side of that same dent.

Formula Entry & Syntax

While most of the tool is visual, you will occasionally need to type formulas (e.g., when using $\✎ P$ blocks or creating custom tasks). To speed this up, the machine supports the following shorthand:

Logical Symbol	LaTeX	Shorthand
Conjunction (And)	$\wedge$	`
Disjunction (Or)	$\vee$	`-`
Implication	$\rightarrow$	`^`
Nor/Nand	$\uparrow$	`~`
Negation (Not)	$\neg$	`!`
Universal Quantifier	$\forall$	`\`
Existential Quantifier	$\exists$	(varies)
Falsity/Contradiction	$\bot$	`--> False`

🏗️ Customization & Tasks

Creating Custom Tasks: To define a task with multiple conclusions or assumptions, simply list each one on a new line:

Assumption 1
Assumption 2
Conclusion 1
Conclusion 2

Creating Custom Blocks: You can group existing logic into a single reusable component. Hold Shift to select multiple blocks, and then select the option to wrap them into a custom block.

💾 Data Persistence

~~Your proofs are stored permanently on a cloud server.~~ Currently, proofs are saved only within your browser's local storage. This means your work will be deleted if:

You clear your browser cache/local storage.
You are using a private/incognito window.

Note: Server-side saving is planned for a future update.

🎓 Credits & Academic References

The project was primarily developed by Joachim Breitner, with support from friends and colleagues.

Academic Publications:

ITP 2016: Visual theorem proving with the Incredible Proof Machine (Accepted paper, Aug 2016).
LFMTP 2016: The Incredible Proof Machine (Invited talk, June 2016).
AFP: The meta theory of the Incredible Proof Machine (Isabelle formalization in the Archive of Formal Proofs, May 2016).
Podcast: Interview with Sebastian Ritterbusch on the German science podcast "Modellansatz" (Episode 78, 2016).

🤝 Contribution

Because this is Free Software, the source code is open for everyone. We encourage you to dive in and contribute—the more help we receive, the more "incredible" the machine becomes!