Aristotle: IMO-level Automated Theorem Proving
Authors:
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-…
▽ More
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.
△ Less
Submitted 10 October, 2025; v1 submitted 1 October, 2025;
originally announced October 2025.
Newclid: A User-Friendly Replacement for AlphaGeometry
Authors:
Vladmir Sicca,
Tianxiang Xia,
Mathïs Fédérico,
Philip John Gorinski,
Simon Frieder,
Shangling Jui
Abstract:
We introduce a new symbolic solver for geometry, called Newclid, which is based on AlphaGeometry. Newclid contains a symbolic solver called DDARN (derived from DDAR-Newclid), which is a significant refactoring and upgrade of AlphaGeometry's DDAR symbolic solver by being more user-friendly - both for the end user as well as for a programmer wishing to extend the codebase. For the programmer, improv…
▽ More
We introduce a new symbolic solver for geometry, called Newclid, which is based on AlphaGeometry. Newclid contains a symbolic solver called DDARN (derived from DDAR-Newclid), which is a significant refactoring and upgrade of AlphaGeometry's DDAR symbolic solver by being more user-friendly - both for the end user as well as for a programmer wishing to extend the codebase. For the programmer, improvements include a modularized codebase and new debugging and visualization tools. For the user, Newclid contains a new command line interface (CLI) that provides interfaces for agents to guide DDARN. DDARN is flexible with respect to its internal reasoning, which can be steered by agents. Further, we support input from GeoGebra to make Newclid accessible for educational contexts. Further, the scope of problems that Newclid can solve has been expanded to include the ability to have an improved understanding of metric geometry concepts (length, angle) and to use theorems such as the Pythagorean theorem in proofs. Bugs have been fixed, and reproducibility has been improved. Lastly, we re-evaluated the five remaining problems from the original AG-30 dataset that AlphaGeometry was not able to solve and contrasted them with the abilities of DDARN, running in breadth-first-search agentic mode (which corresponds to how DDARN runs by default), finding that DDARN solves an additional problem. We have open-sourced our code under: https://github.com/LMCRC/Newclid
△ Less
Submitted 18 November, 2024;
originally announced November 2024.