University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Informal to formal and back with LLMs

  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

Informal to formal and back with LLMs

Download to your calendar using vCal

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

BPRW03 - Big proof: formalizing mathematics at scale

While there has been huge progress in formalization of mathematics over the last few years, the process of formalization is still very tedious. Furthermore, going back-and-forth between informal and formal introduces a lot of friction. LLMs have been improving at a fast pace in their ability to handle formal and informal mathematics and have become a tool of choice in this space. In this talk, we will explore how to use or tune Large Language Models (LLMs) for (large scale) autormalization and auto-informalization tasks and discuss how one could build a tool to help mathematicians interact more naturally with the Lean theorem prover.(based on joint work with Ilya Tolstikhin)

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

Dept of Physiology Main lecture theatre Hybrid: Seminar room, SPRI & Teams - email organiser for details Online via zoom https://zoom.us/meeting/register/tJUrcO6rqDoiHNYhecZbx4ZDYqCzxNMGPMMo

Other talks

Title to be confirmed Spectral theory for Dirac operators with singular potentials An Amphibious Urbanism | | Cut 4: The Desert Arrives Slowly TBC Cambridge RNA Club - IN PERSON Title TBC
 

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