Informal to formal and back with LLMs

Add to your list(s) Download to your calendar using vCal

• Olivier Bousquet (Google DeepMind Technologies Limited)
• Wednesday 11 June 2025, 11:45-12:45
• Seminar Room 1, Newton Institute.

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:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.