[FOM] Solovay's question about the Skewes bound

[Alasdair Urquhart]

On April 17, 2006 02:58 am, Robert M. Solovay wrote:
> On Sun, 16 Apr 2006, Gabriel Stolzenberg wrote:
>
>    (Skewes began
>
> > sometime between 1912 and 1933 and finished in 1955, three years
> > after Kreisel explained how to read a bound out of Littlewood's
> > proof.)
>
> Skewes bound was quite explicit [though large]. Would K. get such an
> explicit bound. How would the size of K.'s bound compare to that of
> Skewes?
>
>  	--Bob Solovay


There is a discussion of this question in Feferman's article 
`Kreisel's "Unwinding" Program' in the book `Kreiseliana'
edited by Odifreddi.  I quote from pp. 258-259:

	Finally -- setting aside the logical aspects (or lack thereof) --
	just considered as a piece of work in analytic number theory,
	no explicit bounds are extracted that one can point to, 
	certainly none that would satisfy the mathematicians interested
	in such matters.  Indeed, one is hard put to say exactly
	what the conclusion of this work is ...

The same volume also contains two very interesting contributions
on explicit bounds extracted from proof theory, one by Charles
Delzell on Kreisel's unwinding of Artin's proof, and another 
by Luckhardt on bounds extracted by Kreisel from ineffective proofs.

Alasdair Urquhart