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.