There are two reasons that completely rigorous formal proofs are only done in systems like these.
Firstly, they can only be done in such systems. Doing them by hand will just produce an enormous document full of technical detail which has far less chance of being error-free than the original semi-formal proof. Without the computer implementation, truly rigorous proof of new, deep theorems is practically impossible.
Secondly, mathematicians writing to be read by mathematicians do not need to do formal proofs, and so they don’t. They need only develop them in enough detail that their readers (and they themselves!) can understand the argument clearly enough to see how the formal underpinnings will work.
These projects are motivated by the desire to do that work on behalf of the mathematics community, and create a growing corpus of verified mathematics. Some at least are working towards the day when every mathematician can use such a system as a working tool, but I think that is a ways off yet.
Lean is another for mathematics. So yeah, I don’t really think this post is correct.
Here’s the link:
https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
Thanks for that addition.
There are two reasons that completely rigorous formal proofs are only done in systems like these.
Firstly, they can only be done in such systems. Doing them by hand will just produce an enormous document full of technical detail which has far less chance of being error-free than the original semi-formal proof. Without the computer implementation, truly rigorous proof of new, deep theorems is practically impossible.
Secondly, mathematicians writing to be read by mathematicians do not need to do formal proofs, and so they don’t. They need only develop them in enough detail that their readers (and they themselves!) can understand the argument clearly enough to see how the formal underpinnings will work.
These projects are motivated by the desire to do that work on behalf of the mathematics community, and create a growing corpus of verified mathematics. Some at least are working towards the day when every mathematician can use such a system as a working tool, but I think that is a ways off yet.