# Aristotle: IMO-level Automated Theorem Proving

Article · Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, Lawrence Wu

- Archive id: arxiv:2510.01346
- Published: 2025-10-01
- Venue: SuperIntelligence - Robotics - Safety & Alignment
- DOI: https://doi.org/10.70777/si.v3i3.18745
- arXiv: https://arxiv.org/abs/2510.01346
- Citations: 2
- Source URL: https://arxiv.org/abs/2510.01346
- PDF: https://arxiv.org/pdf/2510.01346
- Provenance: arxiv

## Abstract

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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

Cited in dossiers:
- [AI for Mathematics & Formal Proof: State of the Field (October 2026)](https://space-kitty.com/dossiers/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.