The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
replyBuzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.
replyIt's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext:
reply> The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.
1kk? Why not say 1M?
replyMore importantly how many years it would take.
reply