[FOM] P NP buzz
Timothy Y. Chow
tchow at alum.mit.edu
Mon Aug 16 10:33:11 EDT 2010
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.
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.
More information about the FOM