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).

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).

Tactics and blocks. Every block has exactly one tactic that puts it in, so a level offers the tactics of its blocks. The other way round it is almost one to one; the exceptions are in the last column.

Taktiken und Bausteine. Jeder Baustein hat genau eine Taktik, die ihn einsetzt; deshalb bietet ein Level die Taktiken seiner Bausteine an. Umgekehrt ist es fast eins zu eins; die Ausnahmen stehen in der letzten Spalte.