University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Aristotle, an AI theorem prover using Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Aristotle, an AI theorem prover using Lean

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Trinity Hall History Society FW11, William Gates Building. Zoom link: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon John Harrison and the solution of the Longitude problem

Other talks

Tea and Coffee Break TBC Caribbean Trip and Cacti Packing the Border: Quail Crates and the Regulation of Animal Movement on the US-Mexico Border, 1910s-1940s Unveiling the curtain with ukubuyisa or go lata: complicated roles of museums and nation states in the cultural repatriation discourse and practice in southern Africa Group Presentation 2
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity