Jonathan Thomm
Abstract
Aristotle, an AI system combining formal verification and informal reasoning, achieves top performance on International Mathematical Olympiad problems using Lean proof search, lemma generation, and a geometry solver.
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.
Community
Technical Report: Aristotle: IMO-level Automated Theorem Proving
This is an automated message from the Librarian Bot. I found the following papers similar to this paper.
The following papers were recommended by the Semantic Scholar API
- Hilbert: Recursively Building Formal Proofs with Informal Reasoning (2025)
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction (2025)
- Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs (2025)
- GenesisGeo: Technical Report (2025)
- LeanGeo: Formalizing Competitional Geometry problems in Lean (2025)
- EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving (2025)
- EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty (2025)
Please give a thumbs up to this comment if you found it helpful!
If you want recommendations for any Paper on Hugging Face checkout this Space
You can directly ask Librarian Bot for paper recommendations by tagging it in a comment:
@librarian-bot
recommend
Models citing this paper 0
No model linking this paper
Datasets citing this paper 0
No dataset linking this paper
Spaces citing this paper 0
No Space linking this paper