BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Scaling up autoformalization - Virtual presentation - Jared Duker 
 Lichtman (Stanford University)
DTSTART:20260331T140000Z
DTEND:20260331T142000Z
UID:TALK245722@talks.cam.ac.uk
DESCRIPTION:Autoformalization has seen remarkable progress very recently. 
 In particular\, Math\, Inc&rsquo\;s agent Gauss has scaled up code generat
 ion by three orders of magnitude in the past year. Notably\, Gauss assiste
 d Viazovska-Hariharan&rsquo\;s led team to formalize the Fields Medal proo
 f of Sphere Packing in dimension 8. In the subsequent week\, Gauss was abl
 e to formalize dimension 24 end-to-end\, as the single largest Lean proof 
 in history.&nbsp\; We are also pleased to share OpenGauss as an open-sourc
 e tool for the community.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR