Theorem Cards

Theorem puzzles

Theorem Cards is a PC puzzle game about proving theorems by playing cards, in a solitaire-like format. You solve puzzles about natural numbers, using tactics common in theorem provers, including rewrite, apply and induction.

Proofs and tactics

Lean formally verifies every solution you build, checking each move almost instantly. The game includes Lean 2, an earlier version of the theorem prover. Some familiarity with mathematical notation is recommended, and in-game help explains the tactics and symbols.