Aristotle: IMO-level Automated Theorem Proving

Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico +18 more
10/1/2025
cs.AIcs.CL

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Towards Autonomous Mathematics Research

82% match1 repo7662026

Formal Mathematical Reasoning: A New Frontier in AI

81% match2024

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

81% match1 repo752025

Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

81% match2024

LeanTutor: Towards a Verified AI Mathematical Proof Tutor

80% match2026

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

80% match2024

Cite this paper

@article{achim2025aristotle,
  title  = {Aristotle: IMO-level Automated Theorem Proving},
  author = {Tudor Achim and Alex Best and Alberto Bietti and Kevin Der and Mathïs Fédérico and Sergei Gukov and Daniel Halpern-Leistner and Kirsten Henningsgard and Yury Kudryashov and Alexander Meiburg and Martin Michelsen and Riley Patterson and Eric Rodriguez and Laura Scharff and Vikram Shanker and Vladmir Sicca and Hari Sowrirajan and Aidan Swope and Matyas Tamas and Vlad Tenev and Jonathan Thomm and Harold Williams and Lawrence Wu},
  year   = {2025},
  eprint = {2510.01346},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2510.01346v2}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2510.01346.svg)](https://codeofpaper.com/paper/2510.01346)

Discussion