University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Formalizing Fermat: how it's going

  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

Formalizing Fermat: how it's going

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Synthetic Biology Cambridge & County Folk Museum, Castle Street Li Ka Shing Centre Theatre, Cancer Research Institute, Robinson Way, Addenbrooke's Hospital

Other talks

Using A Function-Centric Lens to Re-consider Regularisation, Representation Transfer and Geometric Properties of Neural Networks Title to be confirmed Chiral Lattice gauge theories from symmetry disentanglers Group Presentation 1 An Amphibious Urbanism | | Cut 4: The Desert Arrives Slowly Disentangling preventative & ejective AGN feedback on a population basis with simulations, observations & machine learning
 

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