4 ms·

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

11 points by amichail 4y ago

And if so, wouldn't most math proofs be full of errors just like untested code?

_448 4y ago
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.
FabHK 4y ago
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/Constructive_proof https://en.wikipedia.org/wiki/Banach–Tarski_paradox 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 https://www-cs-faculty.stanford.edu/~knuth/faq.html
- xigoi 4y ago
  > There are non-constructive proofs …if you accept the law of excluded middle.
imaginarycoder 4y ago
Math proofs could be fun just check out this video: https://youtu.be/Sgupo9DLMGs https://youtu.be/Sgupo9DLMGs
injb 4y ago
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.
- amichail 4y ago
  Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done.
  - injb 4y ago
    >> Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done. I don't think that's it. As a rule, the tests we write for code don't prove anything in the mathematical sense. They are more along the lines of "OK it didn't break with an input of 6 or 7, now let's try 8". IOW we treat the code like a black box and see how it responds to various inputs. Mathematical proof is a different kind of intellectual activity. It's about showing that one fact is a logical consequence of another. You don't test a proof because the proof is the outcome of testing. But that testing is almost always as general as possible. In code, you might test that a given function works with the numbers 1-100 by trying 1 and 100 and simply assuming that it'll behave the same way for the numbers in the middle. This is often adequate, and it's probably the best you can do anyway, but it's not a proof (except for those specific inputs). A mathematician would instead analyze the implementation of the function to show that it's logically guaranteed to work for 1 <= x <= 100. But then the proof would only exist in their head, or on paper, in human readable form. Can you write automated tests that analyze code in that way? Maybe but that's beyond me.
PaulHoule 4y ago
For my PhD thesis I did a calculation that was something like 50 pages to derive https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530ee 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.
proc0 4y ago
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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- AnimalMuppet 4y ago
  If the program can do something useful while not proving anything interesting, then no, programs are not proofs.
  - baremetal 4y ago
    Proving is objective. Interesting is subjective. Your conclusion doesn't follow from the premises.
    - AnimalMuppet 4y ago
      "Interesting" is subjective. So is "useful". I assert that a useful program is more interesting than a useless one. If it's useful (and interesting) as a program, and uninteresting as a proof, then there is a difference between proofs and programs, not at the level of the Curry-Howard Correspondence, but at the level of human life. As a program it can make your life easier; as a proof it's not going to change anyone's life in any way whatsoever.
- kazinator 4y ago
  Programs in a tiny academic bubble are proofs, where types are logical propositions.
  - deleted 4y ago
    [deleted]
mstep 4y ago
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 https://www.hsozkult.de/searching/id/reb-2446
necovek 4y ago
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.
newprint 4y ago
In fact, you can write proofs as programs. https://leanprover.github.io/ 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.pdf 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://research.microsoft.com/users/lamport/tla/tla.html&type=path 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 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.
cevi 4y ago
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).

11 points by amichail 4y ago

And if so, wouldn't most math proofs be full of errors just like untested code?

_448 4y ago

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.

FabHK 4y ago

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/Constructive_proof https://en.wikipedia.org/wiki/Banach–Tarski_paradox 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 https://www-cs-faculty.stanford.edu/~knuth/faq.html

xigoi 4y ago
> There are non-constructive proofs …if you accept the law of excluded middle.

imaginarycoder 4y ago

Math proofs could be fun just check out this video: https://youtu.be/Sgupo9DLMGs https://youtu.be/Sgupo9DLMGs

injb 4y ago

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.

amichail 4y ago
Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done.
- injb 4y ago
  >> Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done. I don't think that's it. As a rule, the tests we write for code don't prove anything in the mathematical sense. They are more along the lines of "OK it didn't break with an input of 6 or 7, now let's try 8". IOW we treat the code like a black box and see how it responds to various inputs. Mathematical proof is a different kind of intellectual activity. It's about showing that one fact is a logical consequence of another. You don't test a proof because the proof is the outcome of testing. But that testing is almost always as general as possible. In code, you might test that a given function works with the numbers 1-100 by trying 1 and 100 and simply assuming that it'll behave the same way for the numbers in the middle. This is often adequate, and it's probably the best you can do anyway, but it's not a proof (except for those specific inputs). A mathematician would instead analyze the implementation of the function to show that it's logically guaranteed to work for 1 <= x <= 100. But then the proof would only exist in their head, or on paper, in human readable form. Can you write automated tests that analyze code in that way? Maybe but that's beyond me.

PaulHoule 4y ago

For my PhD thesis I did a calculation that was something like 50 pages to derive https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530ee 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.

proc0 4y ago

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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

AnimalMuppet 4y ago
If the program can do something useful while not proving anything interesting, then no, programs are not proofs.
- baremetal 4y ago
  Proving is objective. Interesting is subjective. Your conclusion doesn't follow from the premises.
  - AnimalMuppet 4y ago
    "Interesting" is subjective. So is "useful". I assert that a useful program is more interesting than a useless one. If it's useful (and interesting) as a program, and uninteresting as a proof, then there is a difference between proofs and programs, not at the level of the Curry-Howard Correspondence, but at the level of human life. As a program it can make your life easier; as a proof it's not going to change anyone's life in any way whatsoever.
kazinator 4y ago
Programs in a tiny academic bubble are proofs, where types are logical propositions.
- deleted 4y ago
  [deleted]

mstep 4y ago

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 https://www.hsozkult.de/searching/id/reb-2446

necovek 4y ago

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.

newprint 4y ago

In fact, you can write proofs as programs. https://leanprover.github.io/ 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.pdf 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://research.microsoft.com/users/lamport/tla/tla.html&type=path 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 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.

cevi 4y ago

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).