For grown-ups
AxiomForge builds arithmetic from almost nothing: zero, "the next number" (written S), and two rules for adding. From those, the player proves that 2 + 2 = 4, that adding in either order gives the same answer, that brackets do not matter, and some first facts about multiplying.
Each move is either a legal rewrite with a rule or a hypothesis, the check that both sides are now the same (rfl), or induction on a letter. A tiny checker accepts the move or refuses it with a reason, so there is nothing to argue with and nothing to bluff. It is modelled on the Natural Number Game that mathematicians built for the Lean prover.
There are twenty levels in three worlds. A proved result becomes a rule you can use later. Progress stays in this browser. No account, nothing sent.
What it never does
- No accounts, no ads, no tracking — anything kept stays on this device.
- No streaks, timers to beat, points to chase or leaderboards.
- No chat, and nothing anyone types is sent anywhere.