[FOM] Solution (?) to Mathematical Certainty Problem

[Harvey Friedman]

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 
>muddled?
>
>For instance, is:
>
>123890164571029365109343456822478103948560192834750160594382741092845610 
>923874109348564127893561024938750162938740213964501928734016503945817205 
>961029387401928465019284730196509817230498162054938712043986102983570194 
>283605981720398461095879042387501285630981712734891026509382741092856192 
>837401928560192873410986598475192837409182605349857109238456019283741757 
>283495621039874016501923874106539487120945610923874016520394871034650192 
>834750165049871045610294857023946850198273409283645091823745092836405958 
>712094651412845609387410926519283793685198237401938465067586405986985697 
>459834659182734011001010109183274509236450179231010192939292929383883274 
>929562973415610274938561029748374938759825691720394810365019283740165027 
>493845682739481056029837492794723848472956105017514374589230645598127431 
>752893468573940298364359827340659103847502638459713049623984752093861098 
>273457171717172172717717727371727173727712171113123890164571029365109343 
>456822478103948560192834750160594382741092845610923874109348564127893561 
>024938750162938740213964501928734016503945817205961029387401928465019284 
>730196509817230498162054938712043986102983570194283605981720398461095879 
>042387501285630981712734891026509382741092856192837401928560192873410986 
>598475192837409182605349857109238456019283741757283495621039874016501923 
>874106539487120945610923874016520394871034650192834750165049871045610294 
>857023946850198273409283645091823745092836405958712094651412845609387410 
>926519283793685198237401938465067586405986985697459834659182734011001010 
>109183274509236450179231010192939292929383883274929562973415610274938561 
>029748374938759825691720394810365019283740165027493845682739481056029837 
>492794723848472956105017514374589230645598127431752893468573940298364359 
>827340659103847502638459713049623984752093861098273457171717172172717717 
>727371727173727712171113
>
>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 
>THE SAME NUMBER.
>
>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 
verified?

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