Is writing a math proof like programming without ever running your code?

In fact, you can write proofs as programs. https://leanprover.github.io/ - Lean, very popular proof assistant from Microsoft. There are tons information on it on youtube. Another good paper to look at is `How to Write a Proof` by Leslie Lamport http://lamport.azurewebsites.net/pubs/lamport-how-to-write.p... There he argues that mathematical proofs should be written and structured like software code. Leslie came up with TLA+: http://lamport.azurewebsites.net/tla/tla.html?from=https://r... It can be used to write a proof that algorithm is correct. AWS uses it: https://lamport.azurewebsites.net/tla/amazon-excerpt.html

All the important distributed algorithms were formally verified using proof assistants. The entire field of "formal verification" is nothing but writing proofs to verify correctness of software & hardware. There are tons of lectures on formal verification.

Programs ARE proofs. The types are logical propositions. If the code runs then the propositions are true, although for most programming languages types are very flexible so from the mathematical perspective they aren't proving anything interesting (even though the program is doing something useful). This is the Curry-Howard correspondence between logic and programs: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Two things come to mind:

1. There are non-constructive proofs, ie proofs that show that something exists, but do not provide an example (but rather derive a contradiction from the assumption that it doesn't exist, for example). Those are not really akin to running code. The Banach-Tarski paradox is a particularly striking example: You can decompose a ball into 5 pieces and reassemble them into 2 balls of the same size of the original.

https://en.wikipedia.org/wiki/Constructive_proof

https://en.wikipedia.org/wiki/Banach–Tarski_paradox

2. Don Knuth famously sent a colleague some code with the warning "Beware of bugs in the above code; I have only proved it correct, not tried it."

https://www-cs-faculty.stanford.edu/~knuth/faq.html

For my PhD thesis I did a calculation that was something like 50 pages to derive

https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530e...

using a wavepacket basis parameterized in phase space. I wrote extensive unit tests to confirm everything, I even know I got the signs right.

Errors are really common in “mathematical physics” papers, some of the papers that inspired that work had errors in the middle of long calculations that got past the peer reviewers and probably everybody who didn’t try to reproduce the results.

Although the calculation was correct, the result wasn’t as useful as we’d hoped because we had no idea how to calculate the Maslov index because a periodic orbit in classical mechanics is no longer a periodic orbit when you consider the change in the shape of the wavepacket and with no periodic orbit there is no topological invariant. My thesis advisor and another student were able to reuse the math for something where they didn’t need the Maslov index so it wasn’t a complete loss.

Kind of. But your conclusion is also kind of backwards: code is full of errors because it's not written very mathematically. It usually has side effects. Also, mathematicians are trained to think very carefully about the types of objects, and about domains and images of functions (i.e. the set of possible inputs and outputs) whereas programmers tend to leave gaps and think only loosely about these things. For example you write a function that is declared to take an integer, but then the implementation divides something by that integer. Now it can't be zero, but where do you capture that fact? Or a function is supposed to return a number but it can also return null, which isn't a number.

When you tell a mathematician "this function takes an integer" or "that function always returns a string" they will immediately jump to looking for counterexamples to see if they can break it. They do this because they know that one counterexample breaks a proof. Programmers who think that way tend to produce fewer bugs imo.

Yes. You need spend a lot more time thinking about each line of a math proof than you do about each line of code you write, and you need to develop skills and techniques for catching and correcting errors.

Your ability to catch errors tends to be closely linked to the amount of time you've spent working in a particular area - because you build up a mental suite of test cases to check every claim against. One mistake I see occasionally is jumping into a brand new area of math and moving just as quickly as you would in the old area where you had more expertise, making huge blunders every step of the way. When you enter a new area, you have to go really excruciatingly slowly as you build up the intuition and suite of examples.

Almost every math paper contains an error or two - they are usually easy for an expert to fix (the equivalent of leaving out a semicolon at the end of a line in C++, takes only a moment to fix if you have familiarity with the language - but incredibly frustrating to a user who doesn't know how to make the easy fix).

Proofs are usually peer reviewed extensively, though not always. The incentive there is to write papers on top of existing papers and thus gain sci-points important for an academic career (promotions, grants, project participation...).

Tests in programming are more akin to double entry book-keeping in accounting: you specify the same program twice (not really, you usually have manually precalculated a few cases, but that's roughly the point).

As such, mathematical claims (theorems, lemmas or anything, really) requiring proofs are "integration tested" in applying them elsewhere (basically, they give reasonable results). This implicitely tests their proofs too.

For sure, there are probably a lot of fringe theorems based on invalid proofs.

Writing mathematical proof is like writing code, compiling/interpreting(take your pick), debugging, fixing problems, and testing; all at the same time, and that too in real-time.

That is the reason more people find programming enjoyable but struggle with mathematical proof writing.

Math proofs could be fun just check out this video:

https://youtu.be/Sgupo9DLMGs

i remember vaguely that bettina heintz in her sociological study of the field of mathematics from 2000 noted the growing number of proofs that relied on computer programs as potentially problematic for the field.

https://www.hsozkult.de/searching/id/reb-2446