Why is writing down mathematical proofs more fault-proof than writing computer code?

I have noticed that I find it far easier to write down mathematical proofs without making any mistakes, than to write down a computer program without bugs.

It seems that this is something more widespread than just my experience. Most people make software bugs all the time in their programming, and they have the compiler to tell them what the mistake is all the time. I've never heard of someone who wrote a big computer program with no mistakes in it in one go, and had full confidence that it would be bugless. (In fact, hardly any programs are bugless, even many highly debugged ones).

Yet people can write entire papers or books of mathematical proofs without any compiler ever giving them feedback that they made a mistake, and sometimes without even getting feedback from others.

Let me be clear. this is not to say that people don't make mistakes in mathematical proofs, but for even mildly experienced mathematicians, the mistakes are usually not that problematic, and can be solved without the help of some "external oracle" like a compiler pointing to your mistake.

In fact, if this wasn't the case, then mathematics would scarcely be possible it seems to me.

So this led me to ask the question: What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter?

One could say that it is simply the fact that people have the "external oracle" of a compiler pointing them to their mistakes that makes programmers lazy, preventing them from doing what's necessary to write code rigorously. This view would mean that if they didn't have a compiler, they would be able to be as faultless as mathematicians.

You might find this persuasive, but based on my experience programming and writing down mathematical proofs, it seems intuitively to me that this is really not explanation. There seems to be something more fundamentally different about the two endeavours.

My

Let me offer one reason and one misconception as an answer to your question.

The main reason that it is easier to write (seemingly) correct mathematical proofs is that they are written at a very high level. Suppose that you could write a program like this:

function MaximumWindow(A, n, w):
    using a sliding window, calculate (in O(n)) the sums of all length-w windows
    return the maximum sum (be smart and use only O(1) memory)

It would be much harder to go wrong when programming this way, since the specification of the program is much more succinct than its implementation. Indeed, every programmer who tries to convert pseudocode to code, especially to efficient code, encounters this large chasm between the idea of an algorithm and its implementation details. Mathematical proofs concentrate more on the ideas and less on the detail.

The real counterpart of code for mathematical proofs is computer-aided proofs. These are much harder to develop than the usual textual proofs, and one often discovers various hidden corners which are "obvious" to the reader (who usually doesn't even notice them), but not so obvious to the computer. Also, since the computer can only fill in relatively small gaps at present, the proofs must be elaborated to such a level that a human reading them will miss the forest for the trees.

An important misconception is that mathematical proofs are often correct. In fact, this is probably rather optimistic. It is very hard to write complicated proofs without mistakes, and papers often contain errors. Perhaps the most celebrated recent cases are Wiles' first attempt at (a special case of) the modularity theorem (which implies Fermat's last theorem), and various gaps in the classification of finite simple groups, including some 1000+ pages on quasithin groups which were written 20 years after the classification was supposedly finished.

A mistake in a paper of Voevodsky made him doubt written proofs so much that he started developing homotopy type theory, a logical framework useful for developing homotopy theory formally, and henceforth used a computer to verify all his subsequent work (at least according to his own admission). While this is an extreme (and at present, impractical) position, it is still the case that when using a result, one ought to go over the proof and check whether it is correct. In my area there are a few papers which are known to be wrong but have never been retracted, whose status is relayed from mouth to ear among experts.

StackExchange Computer Science Q#85327, answer score: 251