# Proofs including computer checking for "small" numbers

In number theory there are some proofs which given some bound prove that some statement holds for all natural numbers greater than some $$N$$. This $$N$$ can easily be large, say $$10^{30}$$. So one has to check manually that statement holds for all $$n < N$$. Naturally, you leave this for computer to check.

Now there are couple of things bothering me with this. So, you write an algorithm to check property for all $$n < N$$. How can you prove that the algorithm is correct? Now, I've been thinking about this, and I think I know the answer, but I'm putting this remark here in case someone finds it interesting. It's the same as saying "How do you prove your proof is correct?" So, this is not much of an issue because your algorithm usually has $$100$$ lines or so of code and you can convince yourself that it is correct.

However, there are some things that are concerning me. You compile your code on some machine, and thus, you are relying on the correctness of a lot more things than just your code. And proving correctness of compiler is not only utterly hopeless but also simply wrong because every now and then some bug is reported.

Now, proving correctness of compiler and OS, however much utterly hopeless it seems and wrong it is, at least it is theoretically possible. But, actually you are relying on more than that, you are relying on the physical components of computer to work properly. And this is, at least to my knowledge, impossible to prove correctness for.

For subjects that require less rigourous proofs than mathematics, this is just fine. But I'm wondering is there some mathematical approach to solve this, when dealing with problems such as the one stated at beginning? Is this even something we should care about?

My thoughts are, still better that then manually checking, but it twists my mind to put this kind of proof in the same basket as some proof not involving computer.

• Well, there are two parts to this.1. The validity of the language. This part is easy, since many languages base their logic in mathematical logic systems, so showing their consistency is not hard. 2. The validity of the compiler/OS in evaluating the code. This is usually dealt with by publishing code, so that others can run the code as well to check whether it works. You have to take it on faith that compilers work (which, they usually do on average.) Jul 16, 2019 at 21:15
• You might want to read a great book on the topic, books.google.co.uk/books/about/… Jul 16, 2019 at 21:29
• See en.wikipedia.org/wiki/Kepler_conjecture and follow the links for information about the Flyspeck project: a large endeavour to verify the computations required for Tom Hales's proof of the Kepler sphere-packing conjecture. Jul 16, 2019 at 21:37
• Why would we have confidence in the calculations if they were done by hand? Jul 16, 2019 at 21:45
• Because, then you have limited scope of things you have to believe in. And that is, that "couple" of papers of calculations. As indicated in question, confidence in software is a lot of "papers" and on top of that, proved to be false.. Very rarely, but it happens. On top of that, there is the physical components of computer, which can't even be described in "amount of papers".. Jul 16, 2019 at 21:48