BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Informal to formal and back with LLMs - Olivier  Bousquet (Google 
 DeepMind Technologies Limited)
DTSTART:20250611T104500Z
DTEND:20250611T114500Z
UID:TALK230635@talks.cam.ac.uk
DESCRIPTION:While there has been huge progress in formalization of mathema
 tics over the last few years\, the process of formalization is still very 
 tedious. Furthermore\, going back-and-forth between informal and formal in
 troduces a lot of friction. LLMs have been improving at a fast pace in the
 ir ability to handle formal and informal mathematics and have become a too
 l of choice in this space. In this talk\, we will explore how to use or tu
 ne Large Language Models (LLMs) for (large scale) autormalization and auto
 -informalization tasks and discuss how one could build a tool to help math
 ematicians interact more naturally with the Lean theorem prover.(based on 
 joint work with Ilya Tolstikhin)
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR