The Incredible Proof Machine in Lean

Block Lexicon🔗

The blocks of the game, the rules of natural deduction, in the order they come. Red circles are inputs (what still has to be proved), blue dots outputs (what one gets). Coloured boxes are placeholders for statements (or objects): a box of the same colour is the same statement within one block; once the block is connected, the boxes become the statements.

Die Bausteine des Spiels, die Regeln des natürlichen Schließens, in der Reihenfolge, in der sie kommen. Rote Kreise sind Eingänge (was noch zu beweisen ist), blaue Punkte Ausgänge (was man bekommt). Farbige Kästchen sind Platzhalter für Aussagen (oder Objekte): Ein Kästchen derselben Farbe ist innerhalb eines Bausteins dieselbe Aussage; ist der Baustein verbunden, werden aus den Kästchen die Aussagen.