Formalizing Fermat: how it's going

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

• Kevin Buzzard (Imperial College London)
• Monday 09 June 2025, 10:15-11:15
• Seminar Room 1, Newton Institute.

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

BPRW03 - Big proof: formalizing mathematics at scale

I am running an EPSRC -funded 5 year project which involves teaching a modern proof of Fermat’s Last Theorem to the Lean theorem prover. It has been running for just over 8 months. In the talk I’ll explain more about the goals, and give an overview of how it’s going and the things that we’ve learnt so far. Rest assured that I will not be assuming that the audience knows anything about the technicalities of the proof.  

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.