This time a news is that the previously known value for n = 7, 1371, turned out to be incomplete due to the program bug and it is now thought to equal to 1372 instead.
And the bug was quite silly -- it does a simple standard thing (remove obvious symmetries) in a more complicated way (at the end of a long computation, instead of at the start), incorrectly.
Always good to test code with and without such optimizations to verify the results are the same. That's not always practical though for large problems and optimizations that yield significant time savings.
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/)
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.
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).
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."
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.
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.
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.
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.
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.
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).
> 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.
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.
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.
> but they're rare enough that the they're widely reported in the (mathematical) community.
You should ask math professors how often there are errors in papers. Every one has their own ratio, but I've heard numbers as high as 30%. However, the general belief is the results are still correct, so few are worried about building with a pile of cards.
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.
A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.
This is a bit whooosh for my poor head, but very cool to notice that Greg Egan [1] (an SF author definitely represented in my bookshelves) is active in that scene.
Now we might see this on Leetcode or Hackerrank interviews: "Write a software that takes a number n and outputs the number m, of all different modes a square can be divided into n similar rectangles."
The images I saw in the two articles (original and update) don't look like the rectangles have the same aspect ratio. I didn't measure them, so, yes, I could be wrong.
This time a news is that the previously known value for n = 7, 1371, turned out to be incomplete due to the program bug and it is now thought to equal to 1372 instead.