The puzzles
are real proofs.

Axiom hands you a theorem and a satchel of axioms. You grow the proof by hand, and a verification kernel on your phone checks every step. When it says you proved it, you proved it.

Get it on Google Play

Chess apps did this for chess. Nobody had done it for proof.

Mathematics education is almost entirely arithmetic: the calculating half. The reasoning half, where the beauty actually lives, is taught nowhere outside a university course. It turns out it makes a very good puzzle game.

You work backwards, the way mathematicians do

The theorem sits at the top of the board, unproven. Every move breaks it into something smaller until each branch lands on something already known.

Take the promise. A goal shaped like an arrow becomes a hypothesis you may use, and a smaller thing left to show.
Reach for a tool. Drag an axiom onto a goal. If it fits, the step clicks home. If it does not, it bounces back and nothing is lost.
Ground out. When every leaf rests on something you already hold, the tree lights from the leaves upward and the theorem turns to cut stone.

Twenty five centuries, one map

From Euclid to the infinitude of primes

Forty four theorems across three regions, each one a wax seal on the map. Lemmas you prove become tools you keep, so the game builds mathematics the way mathematics was actually built.

The Grand Map: the mark of the interlocking proof, a progress bar, and a trail of seals through the Riverlands of Geometry. — An open seal is a dark ring. A proved one is cut stone, and a crown on it means you matched the shortest proof the kernel can find without asking for a hint.

A finished proof, every node turned to pale stone with crimson edges, and a result card showing five moves against a par of five. — The cascade fires when the last leaf grounds out and the whole tree turns to cut stone. It is earned by logic and never by luck, which is why it does not get old.

The daily proof screen showing a solved result, the spoiler free shape grid and a thirty day archive. — One theorem a day, the same one for everyone, worked out from the date. The result grid gives away the shape of your proof and nothing else.

Eight moves carry the whole game

You never type mathematics. Every rule of inference is a button with a plain English name, and the kernel underneath is the real thing.

Suppose: Accept what an arrow offers, and owe what it points at.
Prove both halves: Split an “and” into two independent jobs.
Pick a side: Choose which half of an “or” you can actually reach.
Take cases: Handle an “or” you were not allowed to choose, on both branches.
Use: Aim an axiom or an earned lemma at a goal, filling in any terms it leaves open.
Suppose it is false: Proof by contradiction. Hunt for the impossible.
Induction: Prove it of nought, then pass it from every number to the next.
Name it: Fix an arbitrary thing, or produce the witness an “exists” demands.

What is actually in the box

No account, no server, no subscription

A real kernel

Under eight hundred lines of verification code sit beneath the board. It re-checks a finished proof from the root before it counts, and it produced every par in the game by searching for the shortest proof itself. Nothing in the content was scored by hand.

No network

Axiom does not request the internet permission, so Android will not let it open a connection at all. The daily works in flight mode because it is computed from the date, not fetched.

No leaderboards

Ranking players against each other would need an account and a server, and there is neither. Crowns are scored against the kernel's own shortest proof, which is a harder opponent and a more honest one.

Free and complete

Every region, every theorem, the daily proof, the forge and the whole satchel. No purchases, no energy, no advertising, and nothing held back behind a pass. Your record exports to a JSON file and restores from one, which is the only way it ever leaves the phone.