arXiv 2510.01346
Aristotle: IMO-level Automated Theorem Proving
By Tudor Achim, Alex Best, et al.
Published 2025-10-01
Mindmap
Browse the paper's core ideas, clusters, and relationships in a structured outline.
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performa…