Aristotle: IMO-Level Automated Theorem Proving (arxiv.org)

Aristotle is a new hybrid AI system that marries formal proof search in the Lean theorem prover with an informal reasoning layer and a specialized geometry solver, and it reportedly achieves gold‑medal‑equivalent performance on the 2025 International Mathematical Olympiad. The system’s pipeline uses an informal reasoning module to propose high‑level lemmas and strategies, automatically formalizes those lemmas into Lean, and employs a focused proof search engine (plus a dedicated geometry component for Euclidean problems) to produce machine‑checkable proofs. The authors release code, data and demos alongside the paper. For the AI/ML and automated theorem proving communities this is significant because it demonstrates that integrating language‑style mathematical reasoning with rigorous proof assistants can scale to very hard, creative problems that were previously out of reach for pure ATP or LLM approaches. Key technical implications include: (1) the utility of lemma generation and formalization as a bridge between informal human reasoning and mechanized proof search, (2) the value of specialized solvers (geometry) inside a modular architecture, and (3) favorable scaling behavior suggesting further gains as models, proof libraries and search methods improve. Aristotle points toward practical workflows for research assistance, formal verification of human proofs, and more automated discovery in mathematics, while reminding us that careful system design and domain modules remain crucial.