BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Aristotle\, an AI theorem prover using Lean - Alex J Best (Harmoni
 c)
DTSTART:20260129T170000Z
DTEND:20260129T180000Z
UID:TALK243277@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:I'll describe the principles underlying the development of Ari
 stotle\, an AI theorem prover trained via reinforcement learning on Lean p
 roofs\, that acheived a gold medal equivalent score on this years IMO prob
 lems\, has been used to solve open problems and autoformalize new papers i
 n real time. I'll give a demo of how this can be accessed and show some ex
 amples of projects making heavy use of this technology\, in particular tho
 se using it for novel mathematical proofs and for library development. I'l
 l also discuss where (formal) mathematics might be headed as these tools c
 ontinue to develop and evolve\, and how working on mathematics might chang
 e as mathematicians incorporate these tools into their work process.\n\n==
 = Hybrid talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/8985609
 1954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Pas
 scode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR