Is this the Future of Mathematics?

[Jimmy84]

I was reading about some problems in theoretical computer science, and the problem P = NP? is considered to be the most important problem in the field. and it has very deep implications for all of mathematics if proven true.

(Quote)
http://en.wikipedia.org/wiki/P_=_NP_problem#Consequences_of_proof"

One of the reasons the problem attracts so much attention is the consequences of the answer.

A proof of P = NP could have stunning practical consequences, if the proof leads to efficient methods for solving some of the important problems in NP. Various NP-complete problems are fundamental in many fields. There are enormous positive consequences that would follow from rendering tractable many currently mathematically intractable problems. For instance, many problems in operations research are NP-complete, such as some types of integer programming, and the traveling salesman problem, to name two of the most famous examples. Efficient solutions to these problems would have enormous implications for logistics. Many other important problems, such as some problems in Protein structure prediction are also NP-complete;[11] if these problems were efficiently solvable it could spur considerable advances in biology.

But such changes may pale in significance compared to the revolution an efficient method for solving NP-complete problems would cause in mathematics itself. According to Stephen Cook,[12]

...it would transform mathematics by allowing a computer to find a formal proof of any theorem which has a proof of a reasonable length, since formal proofs can easily be recognized in polynomial time. Example problems may well include all of the CMI prize problems.

Research mathematicians spend their careers trying to prove theorems, and some proofs have taken decades or even centuries to find after problems have been stated – for instance, Fermat's Last Theorem took over three centuries to prove. A method that is guaranteed to find proofs to theorems, should one exist of a "reasonable" size, would essentially end this struggle.

A proof that showed that P ≠ NP, while lacking the practical computational benefits of a proof that P = NP, would also represent a massive advance in computational complexity theory and provide guidance for future research. It would allow one to show in a formal way that many common problems cannot be solved efficiently, so that the attention of researchers can be focused on partial solutions or solutions to other problems. (EndQuote)

If the problem is proven true it seems it could take away all the fun that mathematicians had attempting to find proves for math problems, and it may well include a prove for all of the Clay Mathematics Institute prize problems. What do you guys make of this?

 

[Dragonfall]

Even with P=NP, in practice there might not be an efficient theorem prover. For instance, the average case might be n^(2^100) for n the length of the theorem needed to be proven.

 

[Hurkyl]

And besides, mathematics isn't just about proving theorems -- among other things, it is also in the business of figuring out which theorems to prove, and what sorts of things we want to prove theorems about.


For example, there's a beautiful theorem of algebraic geometry (Bezout's theorem) that roughy says if you have two plane curves defined by polynomial equations, then the number of points where they intersect is equal to the product of the degrees of the polynomials.

But to prove that theorem, you can't use a naïve interpretation of "points of intersection": you have to first discover the good definition. The good definition includes counting points with complex coordinates, points "at infinity" in the projective plane, as well as recognizing that curves can intersect multiple times at a single point. (And there's a technical condition to make sure the curves don't have a curve in common)


Two examples of a double intersection at the origin:
(1) The parabola y-x²=0 and the line y=0
(2) the pair of lines xy=0 and the line x+y=0