HackerPapers

arXiv:2510.01346cs.AI

Aristotle: IMO-level Automated Theorem Proving

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

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.

arXiv comments
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence cs.CLComputation and Language

On Hacker News

Linked by 2 identifiable commenters in 5 comments across 2 threads, from Jan 2026 to Jan 2026. Found in 1 HN submission from Oct 2025 to Oct 2025. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. Running Lean at Scale 1 comment

    • This is part of the work that lead to Aristotle, the system that performed at Gold level at IMO: https://arxiv.org/abs/2510.01346

      RGammaView on HNParent context

  2. “Erdos problem #728 was solved more or less autonomously by AI” 4 comments

    • This is great, there is still so much potential in AI once we move beyond LLMs to specialized approaches like this. EDIT: Look at all the people below just reacting to the headline and clearly not reading the posts. Aristotle (https://arxiv.org/abs/2510.01346) is key here folks.…

      D-MachineView on HNParent context

    • It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links?

      D-MachineView on HNParent context

    • It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), as clearly described in Tao's posts.

      D-MachineView on HNParent context

    • Did you not read the parts where Aristotle (https://arxiv.org/pdf/2510.01346) was an integral component of all this?

      D-MachineView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.