Syntactic Sugar v3.2

I'm no specialist in complexity theory but I was thinking about that yesterday… For the moment, the community has no proof of whether P=NP or not. This is one of the most important problem in theoretical computer science.

Using the Coq proof assistant, it is possible to tell whether a proof is true or not, given some context and formalization of a problem. Let's say that we formalize the three following assertions:

• P=NP
• P!=NP
• The P=NP problem is undecidable

The set of all strings is recursively enumerable, so we can go through the set, and test for each string if one of the is a proof of one of the above. Of course this might take an infinite time but who cares?

My point is: Fermat's theorem took several hundred years to be proved, and a few other conjectures are still unproven. Of course, some geniuses are already working on those, but why not try this kind of approach during the same time? If it would give results, that would be great, if it wouldn't, never mind.

Moreover, this whole concept can be really distributed easily, with machines being given strings to check. A few distributed projects, such as SETI@home or Folding@home work pretty well, so why not a P=?NP@home?

As a matter of fact, SETI is a good example: no one knows if something will come out of it, but it's still running.

Of course, if this were to be done, one might say: Hey, don't limit yourself to those 3 questions, you should add this one¹. And this rises the important question of the nature of science and the role of automated computation in that context. Would a proof discovered by a network of PCs have the same value² as a proof written by a human being?

Anyway, this is just useless chatter…

1. where this one could be any conjecture [↩]
2. even though I have no idea of how one would characterize this notion. [↩]