Re: P=NP: Linear Programming Formulation of the TSP

t...@xxxxxxxxxxxxx wrote:
> In article <3de69tF6r1rcoU1@xxxxxxxxxxxxxx>,
> Mitch Harris <harrisq@xxxxxxxxxxxxxxxxxxxxx> wrote:
> >tchow@xxxxxxxxxxxxx wrote:
> >> In article
<1114713726.126023.259970@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
> >> Jennifer Anderson <jen_ander_son@xxxxxxxxx> wrote:
> >>>Why don't they just use computers to check if it's right?
> >> Computers will at most be able to check that the formulation
performs
> >> correctly in a finite number of cases. This won't *prove* that P
= NP.
> >
> >You don't know that!
> >
> >> For that, the argument that this works in general has to be
checked for
> >> logical correctness. And the world is not quite at the stage yet
where
> >> it is routine to write mathematical proofs of nontrivial theorems
in
> >> machine-checkable form.
> >
> >"nontrivial" means no known algorithm. When there is a proven
correct
> >algorithm for a class of problems, those problems then become
trivial.
>
> I suspect we're talking at cross-purposes here.
>
> Jennifer Anderson appears to be suggesting that by implementing
Diaby's
> LP and running it on selected examples, we can verify whether the LP
> is correct. Well, if the LP is wrong, and we run it on an example
where
> we already know the right answer by other means, and the LP gives the
> wrong answer, then indeed we will have settled the matter. But all
> I was saying (in my first three sentences) is that if the LP happens
> to give the right answer on a finite set of cases that we check, then
> this in itself does not prove that the LP is correct and that P = NP.
> There will still be the need for human beings to read Diaby's paper
and
> check its logical correctness.
>
> My fourth sentence addressed the possibility that human beings could
be
> largely replaced by computers even when it comes to the task of
checking
> proofs for logical correctness. I'm not saying this is impossible,
just
> that we're not at the stage yet where this is a routine matter.
Jeremey
> Avigad recently produced a machine-checkable proof of the prime
number
> theorem, but this required a substantial effort on his part and was
not
> "routine." And Thomas Hales estimates that his Flyspeck project for
> producing a machine-checkable proof of the Kepler conjecture will
take
> around 20 person-years.
> --
> Tim Chow tchow-at-alum-dot-mit-dot-edu
> The range of our projectiles---even ... the artillery---however
great, will
> never exceed four of those miles of which as many thousand separate
us from
> the center of the earth. ---Galileo, Dialogues Concerning Two New
Sciences

I meant "WHY DO COMPUTER SCIENTISTS STILL USE HUMANS TO CHECK PROOFS?"
Why can't they program computers to check their proofs? I mean, after
all, they are computer scientists! That way you don't need peer review,
which has lots of flaws, and is obviously inefficient, since it's taken
so long for him to get feedback from the peer reviewers. They should
create a computer language which allows one to write proofs in and
allows the computer to check if they are valid or not. It can't be so
difficult to do. In the modern computer age, it is ironic that computer
scientists still are using the old fashioned way to check their own
work.

Even if it may take a long time to find a proof that P=NP, it only
takes less than a second of computer time to check if it's right.

Jenny :-)

.