4 ms·

As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer

As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. Especially computer generated proofs should be distrusted unless their output is generated as a computer verifiable. Successful example is Flyspeck, that translated a proof with a large computer generated part into a computer readable one (http://www.proof-technologies.com/flyspeck/ http://www.proof-technologies.com/flyspeck/) Computer-readable proofs provide a rigorous and reliable way to verify mathematical results, reducing the likelihood of mistakes and increasing confidence in the validity of mathematical arguments. However, the use of computer-readable proofs is still not widespread in the mathematical community, and it is not yet a standard part of mathematics education. The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated. It should become more widely used in mathematics, and be incorporated into mathematics education curricula at all levels. Doing so will not only help prevent errors but also promote transparency and reproducibility in mathematical research.

DeathArrow 4y ago
>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. What if the algorithms have errors? What if a cosmic ray flips one bit of memory?
- cjfd 4y ago
  100% accuracy will never be achievable. What might be achievable, though, is a higher degree of confidence than we currently have. Of course, the correctness of algorithms should also have to have a computer validated proof.
- nkrisc 4y ago
  > What if the algorithms have errors? Errors will always happen. > What if a cosmic ray flips one bit of memory? Run it several times and compare results until you reach the desired level of statistical certainty.
mkl 4y ago
The tools are not ready. Using proof assistants isn't possible in many areas of maths as the foundational concepts have not yet been built up from fundamental primitives. Even when it is possible, using proof assistants takes far more work, and the proofs are much more verbose and hard for humans to understand. The tools will be ready when the concepts are available for any subfield, when the results are easy to read, and when it takes a reasonable amount of work (ideally it will be faster than doing it by hand).
- martincmartin 4y ago
  I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded. But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."
  - mkl 4y ago
    Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.
- lacker 4y ago
  ideally it will be faster than doing it by hand That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your work. It's easier to type a five page paper in Word than it is to write it longhand. But for now it's a lot more work to encode a proof in a proof assistant than to just write it up in LaTeX (which I think a lot of people don't realize). It's not just that the foundational concepts are missing, it's also that proof assistants currently require you to fill in much more detail than human proofs do. You can't just write something like... "this corollary is trivial", or, "since x is a power of 10, obviously cos(x^2) is irrational"; you have to spell out a proof.
mik1998 4y ago
Is there a proof here at all? The only thing mentioned in the article is a computation. With due respect, computer-readable proofs are not very interesting to me as a mathematician. I don't see why we should do it. Reproducibility is not a concern.
- anonymoushn 4y ago
  Some steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)
- macrolocal 4y ago
  I have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.
  - hgsgm 4y ago
    Most mathematicians don't care about being exactly right. They only need to not see a contradiction. Since most pure math is not used for anything except more math, mistakes rarely have consequences. A computer is only a threat, that might find a mistake that humans miss.
    - macrolocal 4y ago
      This (ahem) contradicts my experience. Most mathematicians I’ve met are excited about formal verification, especially the recent progress toward CFT. Thompson himself has said he’d like his contributions to the classification of finite simple groups verified in his lifetime, and actively followed/encouraged the Coq implementation of his odd order theorem back in 2012.
      - ogogmad 4y ago
        > recent progress toward CFT What's this?
aleks224 4y ago
>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. This seems like a strong overstatement. We got by for more than 2000 years without computer-readable proofs, relying on intuition and validation.
- hgsgm 4y ago
  With lots of major mistakes along the way.
sdfghswe 4y ago
> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, (...) Ironically, computer programs seem to be a lot more error prone than mathematical proofs. Yes, errors in mathematical proofs happen, but they're rare enough that the they're widely reported in the (mathematical) community. Errors in computer programs on the other hand are a virtual guarantee.
- hgsgm 4y ago
  Ironically, emails and essays seem to be out more error prone than mathematical proofs... 1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs. 2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.
- Jeff_Brown 4y ago
  A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.
  - dzdt 4y ago
    The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.
hgsgm 4y ago
> The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated. Seems like a perfect task for an LLM trained on English and Idris/Coq/etc
rssoconnor 4y ago
As another example of this, In [1] I've taken a python program for counting (a bound on) the number of iterations needed of the SafeGCD algorithm to compute a modular inverse for any 256-bit (relatively prime) modulus, translated the python into Coq, and proved the implementation correct. Then by running the computation within Coq we produce a theorem about the bounds (e.g. at most 590 iterations needed for the HD variant of the algorithm). [1] https://blog.blockstream.com/a-formal-proof-of-safegcd-bounds/ https://blog.blockstream.com/a-formal-proof-of-safegcd-bound...

DeathArrow 4y ago

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. What if the algorithms have errors? What if a cosmic ray flips one bit of memory?

cjfd 4y ago
100% accuracy will never be achievable. What might be achievable, though, is a higher degree of confidence than we currently have. Of course, the correctness of algorithms should also have to have a computer validated proof.
nkrisc 4y ago
> What if the algorithms have errors? Errors will always happen. > What if a cosmic ray flips one bit of memory? Run it several times and compare results until you reach the desired level of statistical certainty.

mkl 4y ago

The tools are not ready. Using proof assistants isn't possible in many areas of maths as the foundational concepts have not yet been built up from fundamental primitives. Even when it is possible, using proof assistants takes far more work, and the proofs are much more verbose and hard for humans to understand. The tools will be ready when the concepts are available for any subfield, when the results are easy to read, and when it takes a reasonable amount of work (ideally it will be faster than doing it by hand).

martincmartin 4y ago
I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded. But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."
- mkl 4y ago
  Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.
lacker 4y ago
ideally it will be faster than doing it by hand That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your work. It's easier to type a five page paper in Word than it is to write it longhand. But for now it's a lot more work to encode a proof in a proof assistant than to just write it up in LaTeX (which I think a lot of people don't realize). It's not just that the foundational concepts are missing, it's also that proof assistants currently require you to fill in much more detail than human proofs do. You can't just write something like... "this corollary is trivial", or, "since x is a power of 10, obviously cos(x^2) is irrational"; you have to spell out a proof.

mik1998 4y ago

Is there a proof here at all? The only thing mentioned in the article is a computation. With due respect, computer-readable proofs are not very interesting to me as a mathematician. I don't see why we should do it. Reproducibility is not a concern.

anonymoushn 4y ago
Some steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)
macrolocal 4y ago
I have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.
- hgsgm 4y ago
  Most mathematicians don't care about being exactly right. They only need to not see a contradiction. Since most pure math is not used for anything except more math, mistakes rarely have consequences. A computer is only a threat, that might find a mistake that humans miss.
  - macrolocal 4y ago
    This (ahem) contradicts my experience. Most mathematicians I’ve met are excited about formal verification, especially the recent progress toward CFT. Thompson himself has said he’d like his contributions to the classification of finite simple groups verified in his lifetime, and actively followed/encouraged the Coq implementation of his odd order theorem back in 2012.
    - ogogmad 4y ago
      > recent progress toward CFT What's this?

aleks224 4y ago

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness. This seems like a strong overstatement. We got by for more than 2000 years without computer-readable proofs, relying on intuition and validation.

hgsgm 4y ago
With lots of major mistakes along the way.

sdfghswe 4y ago

> As this incident demonstrates, errors can easily creep into mathematical proofs, even those written by experts. The only way to mitigate this is to use computer-readable proofs, (...) Ironically, computer programs seem to be a lot more error prone than mathematical proofs. Yes, errors in mathematical proofs happen, but they're rare enough that the they're widely reported in the (mathematical) community. Errors in computer programs on the other hand are a virtual guarantee.

hgsgm 4y ago
Ironically, emails and essays seem to be out more error prone than mathematical proofs... 1. Proofs are intended to be correct. The vast majority of computer programs are intended to be practical, and are far far larger than the largest math proofs. Where correctness matters, computer programs have fewer bugs. 2. Nearly every non-computerized mathematical proof is not even a proof, it is a sketch that requires a lot of hand waving and logical jumps to be interpreted. Likewise, specs have fewer bugs than concrete program, because they aren't complete.
Jeff_Brown 4y ago
A math professors blew my mind once by telling me that a paper full of errors was still good work and could be salvaged. He went on to say that most good work was like that. In the worst case you end up proving something else, but typically you can prove what you initially set out for. I found that so strange I had to confirm it with another, who concurred.
- dzdt 4y ago
  The reason for this is that mathematical papers are fundamentally about an insight about mathematical objects. The insight typically comes from the mathematician having a deep understanding of the mathematical objects. The theorems are some formalised statement that should be true based on the deep understanding. The proofs are something else entirely, a sequence of steps which combine to verify the theorem but where many steps may result from trial-and-error searching for a path forward. Coming from a good mathemematician, the original insights are much more likely to be correct than the details of the proof steps.

hgsgm 4y ago

> The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated. Seems like a perfect task for an LLM trained on English and Idris/Coq/etc

rssoconnor 4y ago

As another example of this, In [1] I've taken a python program for counting (a bound on) the number of iterations needed of the SafeGCD algorithm to compute a modular inverse for any 256-bit (relatively prime) modulus, translated the python into Coq, and proved the implementation correct. Then by running the computation within Coq we produce a theorem about the bounds (e.g. at most 590 iterations needed for the HD variant of the algorithm). [1] https://blog.blockstream.com/a-formal-proof-of-safegcd-bounds/ https://blog.blockstream.com/a-formal-proof-of-safegcd-bound...