AlphaGeometry
A system combining a language model with a symbolic deduction engine solved 25 of the 30 geometry problems from the International Mathematical Olympiad within the competition time limit.
Why it matters
Close to the average gold medallist, and reached without a single human solution in the training data.
The symbolic engine derives consequences from the premises until it stalls; then the language model proposes an auxiliary construction, an extra point or line, and deduction continues. The model was trained on a hundred million synthetic problems the system generated itself, with no human proofs at all. It joins two traditions that had competed for forty years: logical deduction gives a guarantee of correctness, and a trained model gives the guess about where to start.