Kevin Buzzard
xenaproject@mathstodon.xyz
<p>Mathematician at Imperial College in London. Interested in number theory and theorem provers.</p>
Posts
-
Post #1366389
One file to go before the main phase of the port of mathlib from lean 3 to lean 4 is complete!
-
Post #1366386
I heard officially yesterday that the EPSRC (the UK science funding body) have awarded me a 5 year research grant to begin the task of formalising a proof of Fermat&#39;s Last Theorem in Lean, an interactive theorem prover! The grant starts in October 2024. I don&#39;t know whether the whole thing can be done in 5 years; I will run it as an open source project and a lot will depend on who else decides to get involved. I am confident that the main objective I highlighted in the grant, na...
-
Post #1366385
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&#39;t at all clear to me w...
-
Post #1366382
I&#39;ve been watching @tao &#39;s approach to running the Polynomial Freiman-Ruzsa formalisation project with interest. This is Terry&#39;s second Lean project; the first was essentially a single-author project, and my understanding is that part of the motivation for embarking on the second was that he wanted to see what a collaborative formalisation experience was like. Having been involved in several of these I would definitely say that they&#39;re great fun and that you learn...
-
Post #1366381
@andrejbauer @tao Only combinatorics. I still maintain that it would be an extremely long project to even *state* the main theorems in any of the recent papers written by Toby Gee or Ana Caraiani, two other number theorists in my department. And proving them would be completely inaccessible -- even proving FLT is a gigantic project and this is from the 90s. There are still lots of problems in the way of making formalisation of all modern mathematics easy.