🧮 AxiomForge

A real case · you decide

Mireya and the obvious

Mireya — a seventeen-year-old in a school maths club

The idea in play: proving a fact for every number at once, from rules, without assuming it.

At maths club a friend laughs: “Everyone knows a + b = b + a. Why would anyone prove it?”

Mireya has the club’s little rule book: zero, “the next number”, and two rules for adding. Nothing else.

Commutativity is not one of the rules. If it is true, it has to follow from them.

Mathematicians now check proofs with programs like Lean for the same reason: a proof should convince a machine that believes nothing.

Try the first level →