Saved in:
Bibliographic Details
Main Authors: Achim, Tudor, Best, Alex, Bietti, Alberto, Der, Kevin, Fédérico, Mathïs, Gukov, Sergei, Halpern-Leistner, Daniel, Henningsgard, Kirsten, Kudryashov, Yury, Meiburg, Alexander, Michelsen, Martin, Patterson, Riley, Rodriguez, Eric, Scharff, Laura, Shanker, Vikram, Sicca, Vladmir, Sowrirajan, Hari, Swope, Aidan, Tamas, Matyas, Tenev, Vlad, Thomm, Jonathan, Williams, Harold, Wu, Lawrence
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2510.01346
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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 performance with favorable scaling properties for automated theorem proving.