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

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
.