Axiom: The Proof Game

Chess apps turned an intimidating discipline into a daily habit for a hundred million people. Axiom does the same for mathematical proof. Every puzzle here is a real theorem. The base angles of an isosceles triangle are equal. A number whose square is even is itself even. There is a prime larger than any number you can name. You prove them by growing a tree of reasoning, one move at a time, and a verification kernel running on your phone checks every step as you make it. REAL PROOFS, REALLY CHECKED There is an actual proof kernel under the board: a small classical natural deduction engine with a first order term language. It refuses any step that does not follow, and before a proof counts it walks the finished tree again from the root and re-derives every branch. Nothing is taken on trust from the interface. It also produced every par in the game by searching for the shortest proof itself, so a gold crown means you matched the machine, not a number somebody typed in. YOU WILL NEVER TYPE MATHEMATICS Eight moves carry the whole game, and each one is a button with a plain English name. Suppose. Prove both halves. Pick a side. Take cases. Use a tool. Suppose it is false. Induction. Name it. Axioms and the lemmas you have earned sit in a satchel at the bottom of the screen; drag one onto a goal and it either clicks home or bounces back. There is no red cross and no buzzer, because a wrong guess in mathematics is just a guess. FROM EUCLID TO THE PRIMES Forty four theorems across three regions. The Riverlands of Geometry is Euclid: congruence, isosceles triangles, parallels, and the bridge of asses that stopped students for eighteen centuries. The Numbered Steppes is parity, divisibility, induction and Euclid's proof that the primes never run out. The Logic Fens is the shape of argument itself, from double negation to Peirce's law. Four of them are keystones with a short illustrated history you can read once you have earned it. THE DAILY PROOF One theorem a day, the same one for everybody, worked out from the date on your device rather than downloaded. That is why it works with the phone in flight mode. When you finish it you get a spoiler free grid of the shape of your proof tree, your move count and the par, ready to drop into a group chat without giving a single step away. Thirty days of archive, and a streak that is quietly counted rather than waved at you. CROWNS FOR ELEGANCE Finishing is not the whole game. Every theorem records your proof length against the shortest one the kernel can find. Match it with no hints and you take a gold crown. Come within two moves and you take silver. Some of the shortest proofs are famous historical gems, and finding one yourself is the best thing in here. HINTS THAT TEACH STRATEGY Three tiers, and none of them hand you the answer. A nudge asks the question a mathematician would ask next. A strategy card names the shape of the argument. A ghost step lets the kernel point at one legal move without placing it. Hints cost nothing except your claim on the gold crown, because knowledge should not be a consumable. THE FORGE Pick a move you want to drill and the forge grows a fresh theorem around it, checks that it can actually be finished, and hands it over. Your grip on each move fades over a few weeks, which is spaced repetition wearing a work apron. WHAT IS NOT IN HERE No account, no sign in, no cloud, no leaderboard, no subscription and no advertising. Axiom does not request the internet permission, so Android will not let it open a connection at all. Everything you do stays in this app's storage on this phone, and you can export the whole record as JSON whenever you like. The game is free and complete: every region, every theorem, every day. Bring a cup of tea. Some of these took people a thousand years.