Aristotle, an AI theorem prover using Lean

Add to your list(s) Download to your calendar using vCal

• Alex J Best (Harmonic)
• Thursday 29 January 2026, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

I’ll describe the principles underlying the development of Aristotle, an AI theorem prover trained via reinforcement learning on Lean proofs, that acheived a gold medal equivalent score on this years IMO problems, has been used to solve open problems and autoformalize new papers in real time. I’ll give a demo of how this can be accessed and show some examples of projects making heavy use of this technology, in particular those using it for novel mathematical proofs and for library development. I’ll also discuss where (formal) mathematics might be headed as these tools continue to develop and evolve, and how working on mathematics might change as mathematicians incorporate these tools into their work process.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• Martin's interesting talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.