Coming soon

About This Game

Practice your math skills by proving theorems, and learn the most common tactics used in theorem provers, such as rewrite, apply and induction.

You do this by playing cards, just like in a game of solitaire.

Solutions are formally verified by Lean

Play thousands of procedurally generated puzzles about natural numbers. Each one comes with a reference solution, and every solution you build is checked by Lean.

The game ships with Lean 2, an earlier version of the theorem prover. It's small and fast, so every move is checked almost instantly.

Learn by playing

Some familiarity with math notation is recommended, but there is plenty of in-game help to get you comfortable with the tactics and symbols, and the interface is designed to make tactics intuitive.

Six levels, a Sandbox and share codes

There are six difficulty levels, from Intro to Master, and a Sandbox mode where you can experiment and create your own theorems. You can also share your solved puzzles using share codes.

AI Generated Content Disclosure

The developers describe how their game uses AI Generated Content like this:

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.