Midas Prover 1.2 solves all six IMO 2026 problems

The International Mathematical Olympiad is the most prestigious competition in mathematical problem solving. This year we pointed Midas Prover 1.2 at all six IMO 2026 problems, and it solved every one of them — with complete proofs machine-verified in Lean 4, compiled against the latest Mathlib.

Every proof in the IMO2026 repository is open for inspection: each problem directory contains the formal statement alongside the completed, machine-checkable solution produced by the prover.

A major step forward from Midas 1.1

Midas 1.1 solved 3 of the 6 IMO 2026 problems. Midas 1.2 solved all six. On the three problems solved by both generations, average runtime fell from 223 minutes to 41 minutes per problem — a 5.4× speedup, alongside a 2× solve rate.

This is the same direction we keep pushing on: provers that work autonomously at the frontier of difficulty, with proofs a compiler checks instead of a person.