Machines That Do Math

Math looks like AI's hardest case: infinite space, zero tolerance for error, no partial credit. But proofs are search — axioms in, theorem out — and search is what modern ML eats when it has a verifier.

AlphaGeometry (2024, Nature, Solving olympiad geometry without human demonstrations) supplied the missing ingredient: a symbolic engine generated 100 million synthetic theorems and proofs, no human examples needed, and a language model trained on them learned to propose the auxiliary constructions — the clever added line or circle — that crack a proof open. The engine then checks every step, so hallucination can't slip through. It solved 25 of 30 olympiad problems, near gold-medalist level; its successor plus AlphaProof reached silver-medal standard on the real 2024 IMO.