University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Scaling up autoformalization - Virtual presentation

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

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

ℹī¸ Information

Scaling up autoformalization - Virtual presentation

Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

OOEW11 - AI for Maths and Open Science

Autoformalization has seen remarkable progress very recently. In particular, Math, Inc’s agent Gauss has scaled up code generation by three orders of magnitude in the past year. Notably, Gauss assisted Viazovska-Hariharan’s led team to formalize the Fields Medal proof of Sphere Packing in dimension 8. In the subsequent week, Gauss was able to formalize dimension 24 end-to-end, as the single largest Lean proof in history.  We are also pleased to share OpenGauss as an open-source tool for the community.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Austin Building Lecture Theatre, Department of Zoology Room 1S3, Donald McIntyre Building, Faculty of Education, 184 Hills Road, Cambridge, CB2 8PQ BAS Seminar Room 1 (http://bit.ly/4pDlm6l)

Other talks

Fairy Tales Packing the Border: Quail Crates and the Regulation of Animal Movement on the US-Mexico Border, 1910s-1940s Ice in a mostly-Arctic Context TBC Title to be confirmed Online Causal Inference Seminar
 

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