formal-proff-is-useless

= Formal proff is useless

The only cases where formal proof of <theorems> seem to have had actual mathematical value is for theorems that require checking a very large number of case, so much so that no human can be fully certain that no mistakes were made. Some examples:
* https://en.wikipedia.org/wiki/Four_color_theorem[Four color theorem]
* <BB(5)>
* <classification of finite simple groups>

Back to article page