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

In article <1114792588.108525.182310@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
Jennifer Anderson <jen_ander_son@xxxxxxxxx> wrote:
>I meant "WHY DO COMPUTER SCIENTISTS STILL USE HUMANS TO CHECK PROOFS?"
[...]
>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.

It can't be so difficult to do, eh? Have you tried it?

People are engaged in projects of this sort. The QED project, Mizar, etc.
It's not as trivial as you make it sound. Take a look at the following two
links to get a sense of the state of the art.

http://www.andrew.cmu.edu/user/avigad/Papers/pntnotes.pdf
http://www.math.pitt.edu/~thales/flyspeck

While I do believe that eventually we'll reach the point where machine
checking of proofs will become routine, we're simply not there yet. A lot
more work needs to be done.
--
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
.