[FOM] Harvey's effective number theorists

[Harvey Friedman]

On 4/12/06 3:12 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:
 
>  Harvey seems to be right about Roth's theorem and Falting's.

I have been constantly arguing with people on the FOM from its beginning in
1997 till this day. I don't recall a SINGLE case where someone has openly
and unequivocably stated that I was right about a matter that was not
completely formal. You have come as close as anyone (but note your word
"seems").  

>  However, it remains to be checked whether number theorists mean
> the same thing by these words that Harvey does.  They are, after
> all, classical mathematicians and "effective algorithm" is a term
> used by classical mathematicians not constructivists.

I don't know what you have in mind for a possible difference between how I
use the relevant words and how number theorists use the relevant words. I
would like to hear.
> 
>                       Some Personal Comments
> 
>  If, as Harvey suggests and his evidence seems to support, there is
> an "intrinsic" interest in "effective" bounds and algorithms, then
> I'm disappointed.

I have been curious to know why you are disappointed. I am elated.

>  I haven't followed these matters since the late
> 1970's but I confess that I had allowed myself to assume that number
> theorists would have learned better by now.

This makes me even more curious.
 
>  Thinking back to that time, I wonder what Harvey would have made
> of the case of a sign change for pi - li, with Littlewood's classical
> proof and Skewes' number as the bound.  For a time, it was the most
> famous case of this kind.  One can read about it in Ingham's "On the
> Distribution of Prime Numbers" and, on the web, in Marcus du Sautoy's,
> "The Music of the Primes" (127-131).

pi(x) is the number of primes <= x. Li(x) is the integral from 2 to x of
du/ln(u). 

I found the following excerpt from

http://numbers.computation.free.fr/Constants/Primes/countingPrimes.html

"Riemann and Gauss believed that Li(x) > p(x) for every x > 3, and all the
computed values of Li(x) - p(x) today satisfy this inequality. However it
has been proved by Littlewood in 1914 that Li(x) - p(x) changes its sign
infinitely  often. In 1933, S. Skewes established that the first change of
sign occurs before the impressive number 10^k with k = 10^10^34 . This
bound has been improved in 1966 by R.S. Lehman who gave the bound 10^1166.
Later in 1985, H. Te Riele proved that the first change of sign occurs
before x = 6.69 x 10^370.  The best bound known so far has been obtained in
2000 by Carter Bays and Richard H. Hudson [1] who proved that the first
change of sign occurs before x = 1.39822 x 10^316 . Of course, such a large
value is not reachable today, but the function Li(x) - p(x) have large
variations in the last table values, suggesting that a change of sign could
occur not too far from this zone. The Li(x) - p(x) project could afford the
first known value x for which p(x) > Li(x) ! Finding the first change of
sign is even more difficult !"

This is obviously something to be proud of. It starts off with a "not
desirable bound", which has gradually over the years, become somewhat more
desirable. There is the big open problem of seeing if the bound can be made
much better. 
> 
>   I also wonder what Harvey would have made of a brief exchange I
> once had with Harold Stark about a first cousin to pi - li that he
> had just proved.  In the exchange, he played the role of Littlewood
> and the question was whether we also needed a Skewes.

I can't make anything of this from what you wrote.
> 
>                        The Classical Proof
> 
>  In Harvey's setup, there is always a classical proof.  I would
> like to know more about the role that having a classical proof plays
> in making a number theorist want a constructive one and also about
> the role that having no proof plays in making him seek a classical
> one.

Are you talking about Pi03 or Pi02? I don't think I understand these
questions.
> 
>                   How Effective is "Effective"?
> 
>  What are some good examples of a number theorist's "effective"
> bounds and algorithms helping him to get realistic ones?  Help that
> he can't get just as easily from the classical proof.

All of the examples I mentioned did not involve any distinction between
classical proofs and constructive proofs. The people involved just rolled up
their sleeves and got better and better bounds without regard to any methods
involved. Of course, we are in the region here where my A-translation kicks
in, so that we know in principle that classical proofs can be automatically
converted to constructive proofs. Probably this is easy to do in the cases
at hand, with minimal thought.
> 
>  Finally, I'd like to thank Harvey's first unnamed number theorist
> for his comments and invite him to explain what makes the question of
> getting an "effective" version of Falting's theorem that yields an
> "effective" algorithm" for finding all rational points a "fundamental"
> problem?

This particular number theorist explicitly did not want his name mentioned,
and so he is not going to send a message. Also, my clear impression is that
he regards it as obviously fundamental, and will not provide any more
explanation. 

Harvey Friedman