[FOM] Solution (?) to Mathematical Certainty Problem

Harvey Friedman friedman at math.ohio-state.edu
Sun Jun 22 14:20:07 EDT 2003

Reply to Lindauer 1:06PM 6/21/03.

>How does this avoid the possibility that the underlying hardware has 
>a  systematic but humanly undetectable flaw?  Your system is good 
>for  those mathematical problems which people can see are correctly 
>solved  (e.g. "Looks right to me.").  What about ones with large 
>numbers or  minute fractions where our intuitions tend to become 
>For instance, is:
>Prime or not? 	If not, what is the next highest prime?
>We can imagine a long text file, a log of all the prime numbers less 
>than THAT and the proofs that they are the prime numbers, and then 
>the  next prime number, listed, and if it is identical with THAT, we 
>MIGHT  be able to check it by looking at it (I for one can't 
>memorize numbers  more than 10 digits reliably... being a little 
>dumb). So in order to  verify that THAT number is not in the list, 
>we'd have to use a  computer, but that computer would be subject to 
>the same problem, that  we couldn't verify that it was talking about 
>And even if some savant COULD memorize such numbers, how would we 
>verify their magical ability to memorize numbers and so on?
>The point is simple, what improvement over the ordinary "looks like 
>a  proof to me" is your method?

There seems to be no problem. See the postings of Jones 7:31AM 
6/21/03, Jones 5:36PM 6/21/03, Wiedjk, 8:17PM 6/21/03, Vestergaard 
11:07AM 6/22/04.

Intuition plays no role in this. Perhaps you doubt if any 
hardware/software system, no matter how low level, can be truly 

For example, I want to build a system that can tell whether or not a 
given input string of length 1 billion is a palindrome. I.e., is the 
same as its reverse. And I want to verify that system. Custom built 
hardware. You doubt if this can be done?

I wouldn't trust unaided humans to tell me whether or not a given 
input string of length 1 billion is a palindrome.

The idea is to reduce proof checking to things like this.

Harvey Friedman

More information about the FOM mailing list