Source: cirosantilli/formal-proof-is-useless
= Formal proof is useless
= Formal proff is useless
{synonym}
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>