3 ms·
There's not much that's new here - Freek Wedijk estimated the cost of formalizing the undergrad math curriculum in its entirety at 140 man-years, for a rough mo
by 0815test 8y ago
There's not much that's new here - Freek Wedijk estimated the cost of formalizing the undergrad math curriculum in its entirety at 140 man-years, for a rough monetary cost well above the millions-of-dollars range - link @ https://www.cs.ru.nl/~freek/notes/index.html https://www.cs.ru.nl/~freek/notes/index.html Expensive to be sure, but not excessively so for a mostly one-time effort. Part of the problem though is that we are still far from having a reasonably-standard platform for formal math that could be expected to fully unlock its benefits. Most of the effort in formalization so far seems to be occurring in domains of "synthetic mathematics", which seem to be mostly self-contained and don't take much formalization effort to reach close to the research frontier.
- philipkglass 8y agoBillions of dollars? If it only takes 140 man-years that implies more than $14 million per man-year.
- 0815test 8y agoYup, I suppose that it's closer to the hundreds-of-millions range for the undergrad curriculum only, in a single system - maybe even a bit less than that. But that then leaves open the question of how to go the rest of the way to the actual research frontier in whatever domains of math you care about, plus the inherent uncertainty as to whether these efforts will in fact be useful, since these systems are in such an early state. You're right though that the way I phrased that was a bit confusing, so thanks!