[FOM] P NP buzz

[Timothy Y. Chow]

Harvey Friedman wrote:

>So it might be valuable to
>
>a. Flesh out both theoretically and practically what a "completely  
>detailed proof" is  - still well short of "ultimately rigorous proof"  
>which we know a lot about already.
>b. Give examples of "completely detailed proofs".
>c. Instill this in the educational process. E.g., all Ph.D.s in  
>theoretical mathematical areas must have written a substantial  
>"completely detailed proof".

Lamport's "structured proofs" are a step in this direction.

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

While your proposal might indeed be valuable, I don't think it will 
forestall the problems that you were complaining about.  Lamport writes:

>Computer scientists are more willing to explore unconventional proof 
>styles. Unfortunately, I have found that few of them care whether they 
>have published incorrect results. They often seem glad that an error was 
>not caught by the referees, since that would have meant one fewer 
>publication. I fear that few computer scientists will be motivated to use 
>a proof style that is likely to reveal their mistakes. Structured proofs 
>are unlikely to be widely used in computer science until publishing 
>incorrect results is considered embarrassing rather than normal.

I think Lamport's sweeping generalization of "computer scientists" is 
unfair, but it is certainly true that no "system" for writing proofs will 
solve what is largely a sociological issue.  Would Wu-Yi Hsiang or Grigori 
Perelman have written "completely detailed proofs" or "structured proofs" 
if they had been properly educated?  I doubt it.  In my opinion, the issue 
is not that they don't know what a "completely detailed proof" is; the 
issue is that, for whatever reason, they were not willing to produce one.

On the other side of the coin, the so-called "stars and superstars" whose 
wasted time you bemoan were under no obligation to drop what they were 
doing and study Deolalikar's manuscript.  They did so because they chose 
to.  If you think they made the wrong choice, then I think the primary 
target of your criticism should be the stars and superstars themselves who 
made that choice.  Some secondary criticism can be directed at the people 
who overhyped the proof, but hyping something is not the same as coercing 
people to pay attention to it.

Tim