Buzzard 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.

The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.

More importantly how many years it would take.