Ask HN: Is writing a math proof like programming without ever running your code?
And if so, wouldn't most math proofs be full of errors just like untested code?
24 comments
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.
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...
Programs in a tiny academic bubble are proofs, where types are logical propositions.
[deleted]
If the program can do something useful while not proving anything interesting, then no, programs are not proofs.
Proving is objective.
Interesting is subjective.
Your conclusion doesn't follow from the premises.
Interesting is subjective.
Your conclusion doesn't follow from the premises.
"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.
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.
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
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
> There are non-constructive proofs
…if you accept the law of excluded middle.
…if you accept the law of excluded middle.
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.
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.
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.
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 suspect that people with higher IQ can probably write code with fewer errors when no testing is done.
>> 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.
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.
Quickcheck is a Haskell testing library which allows the programmer to write propositions about how a function should behave, and the library will try to find cases which falsify the proposition.
If my understanding is correct, it can't "prove" any properties, only disprove them.
For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example.
https://github.com/nick8325/quickcheck https://www.idris-lang.org/
If my understanding is correct, it can't "prove" any properties, only disprove them.
For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example.
https://github.com/nick8325/quickcheck https://www.idris-lang.org/
> If my understanding is correct, it can't "prove" any properties, only disprove them.
Almost. If your generators exhaust the input space then the property is proved.
Almost. If your generators exhaust the input space then the property is proved.
"It didn't break with inputs 6 and 7" cannot be ruled out as a non-mathematical statement.
Testing can be combined with inductive reasoning to validate code. Say we have some recursive function with 7 base cases, and a recursive case. We can use testing to validate the 7 base cases, and then an inductive argument that the recursive case is correct.
Testing can be combined with inductive reasoning to validate code. Say we have some recursive function with 7 base cases, and a recursive case. We can use testing to validate the 7 base cases, and then an inductive argument that the recursive case is correct.
Yes you're right. But then you're doing that by analyzing the implementation, not treating it as a black box.
Personally I think we (software developers) should do more of that - i.e. take implementation details into account when designing tests, instead of treating components as black boxes, and when we change those implementation details, examine the tests to see what assumptions were made that now need to change. It's harder but it's closer to really proving something general about the code.
Personally I think we (software developers) should do more of that - i.e. take implementation details into account when designing tests, instead of treating components as black boxes, and when we change those implementation details, examine the tests to see what assumptions were made that now need to change. It's harder but it's closer to really proving something general about the code.
That's where TDD falls down, iin fact. In TDD you first write a black-box test which fails, and then make it pass by fiddling with the interior of the white box. So, good, you then have a nice white-box test. The problem is with the refactoring step. Refactoring keeps the tests working, but some of them turn into blackbox tests which no longer relate to the internals.
Like say you develop a function by adding cases, TDD style. Then you see there is a generality there and refactor so the individual cases go away. The tests probing those cases still have validity, but no value.
Like say you develop a function by adding cases, TDD style. Then you see there is a generality there and refactor so the individual cases go away. The tests probing those cases still have validity, but no value.
The person with the highest IQ in the bunch will refuse to write code when no testing is to be done.
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).
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.
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.
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
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
https://www.hsozkult.de/searching/id/reb-2446