University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > Formalising (part of) the Diagonal Ramsey Paper

Formalising (part of) the Diagonal Ramsey Paper

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

If you have a question about this talk, please contact Anand Rao Tadipatri.

Last March, a paper appeared on arXiv announcing a dramatic advance in Ramsey theory: an exponential reduction in the upper bound for Ramsey numbers. Last November, Bhavik Mehta announced that he had formalised the paper (in Lean), even before the referees had finished checking it. This talk describes a partial formalisation of the same paper within Isabelle. It includes a quick review of Ramsey’s theorem, an outline of the paper and comments on the mathematics therein, and some notes on the formalisation itself.


WATCH ONLINE HERE : Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity