> > "It will probably cost hundreds of millions of pounds worth of > person-hours to digitise any one of the known proofs of Fermat’s Last > Theorem, and once digitised, these proofs will need maintaining, like any > software, which will cost more money." > A curious estimate - I wonder why he thinks it would be that much.
We could compare it with known formalizations of large theorems, for instance, Feit-Thompson theorem. As a crude estimate, the effort took 6 years and 10 full-time workers (the number of authors in https://hal.inria.fr/hal-00816699/document :-) ). At the average pay in US being ~56000$ and one pound being ~1.3$, the total cost of the project amounts to about 2.5 million pounds. Now, the original proof of odd order theorem took 255 journal pages, and Wiles' proof of Fermat's Last Theorem is about 130 pages long, so it's hard to say if its hypothetical formalization should indeed cost "hundreds of millions". The background needed for the Feit-Thompson theorem is quite wide, but it might be the case that it's even wider for Fermat's Last Theorem, so who knows. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/51475501-681a-46bc-9437-a3eb61435823%40googlegroups.com.
