Or to put it more provocatively: proofs are not necessary if we find alternative ways of gathering the same amount of evidence.
In mathematics, there are no alternative ways that give anything like the strength of an actual proof. The mushy sort of thing that is called “evidence” in most other contexts is worthless for mathematics, except so far as it may guide one’s intuition towards finding interesting things.
Computers are mathematics made flesh, and if a transistor had only a probability of 0.99 (generally considered “high” elsewhere) of correctly opening or closing in response to its gate signal, computers as we know them would be impossible. The actual probability has many more 9s on the end, unheard of anywhere else.
Now, it is frequently observed, including in one of the other comments here, that mathematicians generally do not write out proofs in complete detail. However, any competent mathematician can, and far from it being “almost unknown” to do so, there are several major projects extant to do exactly that for all of mathematics. The ones that spring to my mind are CoQ, HOL, Isabelle, and Mizar. There may be others.
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.
In mathematics, there are no alternative ways that give anything like the strength of an actual proof. The mushy sort of thing that is called “evidence” in most other contexts is worthless for mathematics, except so far as it may guide one’s intuition towards finding interesting things.
Computers are mathematics made flesh, and if a transistor had only a probability of 0.99 (generally considered “high” elsewhere) of correctly opening or closing in response to its gate signal, computers as we know them would be impossible. The actual probability has many more 9s on the end, unheard of anywhere else.
Now, it is frequently observed, including in one of the other comments here, that mathematicians generally do not write out proofs in complete detail. However, any competent mathematician can, and far from it being “almost unknown” to do so, there are several major projects extant to do exactly that for all of mathematics. The ones that spring to my mind are CoQ, HOL, Isabelle, and Mizar. There may be others.
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.