Theorem Cards

AI was used to generate about one thousand seed puzzles that ship with this game (these seeds are based on real theorems included in the Lean 2 project). Every seed was verified by Lean and reviewed to make the steps easier to follow. Our own puzzle generator then makes each puzzle more complex by adding up to six extra tactics to its solution (nine supported tactics: rewrite, apply, existsi, left, right, symmetry, constructor, cases and intro). Using AI was important to make the puzzles more challenging and to add tactics not available in our generator, such as induction, contradiction and have. No content is generated by AI while the game is running.