Back

Thanks a lot to Bhavik Mehta, who over the summer completely formalised the breakthrough new Campos-Griffiths-Morris-Sahasrabudheupper upper bounds on Ramsey numbers in Lean, and then wrote a guest post about it for my blog https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ .

This is nontrivial research level mathematics (which was featured in Quanta, Nature etc) being formalised in real time, something which it wasn't at all clear to me would be possible 6 years ago when I started looking at theorem provers. Right now though, the ability to formalise breakthrough results in some given area depends highly on the area. The London Number Theory Seminar talk last Wednesday was about local-global compatibility in a torsion Langlands correspondence https://researchseminars.org/talk/LNTS/115/ and no theorem prover is remotely near even *stating* the results which were announced in that seminar, let alone proving them. My future work on formalising a proof of Fermat's Last Theorem will hopefully start addressing these matters.