3 ms·

But maybe Euclid could have accomplished more in life with programming?

PaulHoule 5y ago
In some sense yes. The two also can go together like peanut butter and jelly. When I was in grad school my thesis contained a derivation of the Gutzwiller trace formula https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530ee https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530e... integrating over phase space instead of position space (that paper does it over position space.) It was about 40 pages worth of math and while I wrote the math I also wrote each equation in a computer program that would try different inputs and check that the equality held. This didn't "prove" anything, but it convinced me that I had the math right. When you do a calculation like that you might have 50+ places where there might be or might not be a minus sign and if you make any mistakes you might as well flip the coin to get the sign. I could have done the calculation without writing the program but I would have either gotten the wrong answer (not so likely in this case because I knew what the answer was) or gotten the right answer in the wrong way.
Brian_K_White 5y ago
He could write programs that find more primes, but never one that proves there will always be an infinite supply of primes. I think other comments already said it. "more" is an ambiguous term. Do whatever you want and feel free to call that "accomplishing more".
- jakear 5y ago
  Wait what? Computer science encompasses mathematics. Any proof that can be validated by following a known set of reduction steps until axiomatic statements are reached (i.e. any proof worth the paper it’s written on) can be verified just as well by a computer as a person. For your specific case: definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in have m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), have m + 1 ≥ 2, from succ_le_succ this, obtain p `prime p` `p ∣ m + 1`, from sub_prime_and_dvd this, have p ≥ 2, from ge_two_of_prime `prime p`, have p > 0, from lt_of_succ_lt (lt_of_succ_le `p ≥ 2`), have p ≥ n, from by_contradiction (suppose ¬ p ≥ n, have p < n, from lt_of_not_ge this, have p ≤ n + 1, from le_of_lt (lt.step this), have p ∣ m, from dvd_fact `p > 0` this, have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this, have p ≤ 1, from le_of_dvd zero_lt_one this, absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial), subtype.tag p (and.intro this `prime p`) https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/ https://homotopytypetheory.org/2015/12/02/the-proof-assistan...
  - Jensson 5y ago
    Writing proofs in proof assistants is still harder than writing regular proofs despite all efforts done to make it simpler, so I doubt that Euler would have managed to prove much if he tried to do it via computer programs instead. Not to mention what it does to readability, humanity would never have gotten anywhere if mathematicians produced proofs looking like that. I'm not sure why programmers say mathematicians write hard to read stuff, when programmers trying to do the same thing comes up with that.
    - jakear 5y ago
      If Euclid had formulated his proof from axioms rather than intuition it would a) be an actual proof and b) far exceed the length of the above snippet.
      - Jensson 5y ago
        The code you provided is only a proof if you can convince the reader that the code actually corresponds to Euclids theorem, otherwise it could be full of bugs. You could argue that it is less likely to have bugs than the original theorem, but I disagree, the original theorem has stood for over a century and checked by countless mathematicians and is just a few lines, there is no codebase in existence as well checked as that. There are thousands of lines of CoQ dependencies for your snippet to run, and then many more lines in the CoQ compiler/runtime. The probability that all of that is bug free is much less than the probability that Euclids original proof is right. Theorems written by mathematicians are virtually bug free compared to code written by computer scientists. Until you solve that problem coded proofs doesn't really add any validity to proof, it could still be reviewed like a real proof, but then you are just using circular logic that your code is proven to be correct by expert checkers, exactly like how mathematical proofs are proven to be correct by expert checkers. Maybe the reviews are a bit easier then, but you still have the reviewers as a weak link, so there is no difference in theory, a buggy implementation will still lead to buggy results in both cases. And no, you don't have to show all the steps for it to be a real proof. just like you don't have to plant apple seeds to make an apple pie, as long as the knowledge exists out there you can rely on it, just like your coq snippet relies on other coq code and isn't a proof on its own, relying on existing knowledge is a feature and not a bug. Edit: And if you still disagree, the fact that theorem provers haven't disproven any famous mathematical result yet means that the old way actually produced reliable proofs. And as far as we know the people who wrote the theorem prover proofs maybe missed some things and they proved different things, and only stopped once they got the same results as the mathematicians. We don't know, maybe they are right, but I wouldn't be surprised if some of those proofs actually missed some important aspects and proved weaker results. It is enough that a single of your dependencies didn't write their theorem correctly and every proof depending on it is now wrong.

In some sense yes. The two also can go together like peanut butter and jelly. When I was in grad school my thesis contained a derivation of the Gutzwiller trace formula https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530ee https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530e... integrating over phase space instead of position space (that paper does it over position space.) It was about 40 pages worth of math and while I wrote the math I also wrote each equation in a computer program that would try different inputs and check that the equality held. This didn't "prove" anything, but it convinced me that I had the math right. When you do a calculation like that you might have 50+ places where there might be or might not be a minus sign and if you make any mistakes you might as well flip the coin to get the sign. I could have done the calculation without writing the program but I would have either gotten the wrong answer (not so likely in this case because I knew what the answer was) or gotten the right answer in the wrong way.

Brian_K_White 5y ago

He could write programs that find more primes, but never one that proves there will always be an infinite supply of primes. I think other comments already said it. "more" is an ambiguous term. Do whatever you want and feel free to call that "accomplishing more".

jakear 5y ago
Wait what? Computer science encompasses mathematics. Any proof that can be validated by following a known set of reduction steps until axiomatic statements are reached (i.e. any proof worth the paper it’s written on) can be verified just as well by a computer as a person. For your specific case: definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in have m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), have m + 1 ≥ 2, from succ_le_succ this, obtain p `prime p` `p ∣ m + 1`, from sub_prime_and_dvd this, have p ≥ 2, from ge_two_of_prime `prime p`, have p > 0, from lt_of_succ_lt (lt_of_succ_le `p ≥ 2`), have p ≥ n, from by_contradiction (suppose ¬ p ≥ n, have p < n, from lt_of_not_ge this, have p ≤ n + 1, from le_of_lt (lt.step this), have p ∣ m, from dvd_fact `p > 0` this, have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this, have p ≤ 1, from le_of_dvd zero_lt_one this, absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial), subtype.tag p (and.intro this `prime p`) https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/ https://homotopytypetheory.org/2015/12/02/the-proof-assistan...
- Jensson 5y ago
  Writing proofs in proof assistants is still harder than writing regular proofs despite all efforts done to make it simpler, so I doubt that Euler would have managed to prove much if he tried to do it via computer programs instead. Not to mention what it does to readability, humanity would never have gotten anywhere if mathematicians produced proofs looking like that. I'm not sure why programmers say mathematicians write hard to read stuff, when programmers trying to do the same thing comes up with that.
  - jakear 5y ago
    If Euclid had formulated his proof from axioms rather than intuition it would a) be an actual proof and b) far exceed the length of the above snippet.
    - Jensson 5y ago
      The code you provided is only a proof if you can convince the reader that the code actually corresponds to Euclids theorem, otherwise it could be full of bugs. You could argue that it is less likely to have bugs than the original theorem, but I disagree, the original theorem has stood for over a century and checked by countless mathematicians and is just a few lines, there is no codebase in existence as well checked as that. There are thousands of lines of CoQ dependencies for your snippet to run, and then many more lines in the CoQ compiler/runtime. The probability that all of that is bug free is much less than the probability that Euclids original proof is right. Theorems written by mathematicians are virtually bug free compared to code written by computer scientists. Until you solve that problem coded proofs doesn't really add any validity to proof, it could still be reviewed like a real proof, but then you are just using circular logic that your code is proven to be correct by expert checkers, exactly like how mathematical proofs are proven to be correct by expert checkers. Maybe the reviews are a bit easier then, but you still have the reviewers as a weak link, so there is no difference in theory, a buggy implementation will still lead to buggy results in both cases. And no, you don't have to show all the steps for it to be a real proof. just like you don't have to plant apple seeds to make an apple pie, as long as the knowledge exists out there you can rely on it, just like your coq snippet relies on other coq code and isn't a proof on its own, relying on existing knowledge is a feature and not a bug. Edit: And if you still disagree, the fact that theorem provers haven't disproven any famous mathematical result yet means that the old way actually produced reliable proofs. And as far as we know the people who wrote the theorem prover proofs maybe missed some things and they proved different things, and only stopped once they got the same results as the mathematicians. We don't know, maybe they are right, but I wouldn't be surprised if some of those proofs actually missed some important aspects and proved weaker results. It is enough that a single of your dependencies didn't write their theorem correctly and every proof depending on it is now wrong.