Silver at the International Mathematical Olympiad
AlphaProof and AlphaGeometry 2 solved four problems out of six and scored 28 points out of 42, one point below the gold medal threshold.
Why it matters
A machine first got through olympiad mathematics at the level of a strong human contestant, rather than through one section of it.
AlphaProof states the problem in Lean, where every step is machine-checked, and learns by self-play: it generates candidate proofs, checks them, and reinforces on those that pass. AlphaGeometry 2 took the geometry problem. The system solved three problems completely, including the hardest, which only five human contestants managed. The caveat was time: people are given nine hours, and one problem took the system days.