Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2510.01346 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866918158499053568 |
|---|---|
| author | 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 |
| author_facet | 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 |
| 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_01346 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Aristotle: IMO-level Automated Theorem Proving 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 Artificial Intelligence Computation and Language 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. |
| title | Aristotle: IMO-level Automated Theorem Proving |
| topic | Artificial Intelligence Computation and Language |
| url | https://arxiv.org/abs/2510.01346 |