 |
ML Newsnew | past | best | rss | submit | about |
| Aristotle: IMO-Level Automated Theorem Proving (arxiv.org) | |
| 3 points by jasondavies on Oct 3, 2025 | hide | past | pdf | discuss on HN | |
|
In plain words: Aristotle pairs a computer-checked proof search with a free-form reasoner that suggests useful lemmas and turns them into checkable steps, plus a separate solver for geometry. It solved enough of the 2025 International Mathematical Olympiad problems to match a gold medal. Abstract · Aristotle: IMO-level Automated Theorem ProvingWe 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. | |
| add comment on HN |