Formal proof is useless
New to topics? Read the documentation here!
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: