3 ms·

A professor once defined a proof as "That which is convincing", and we were free to say, "I am not convinced" While the topic being proven may be technically c

A professor once defined a proof as "That which is convincing", and we were free to say, "I am not convinced" While the topic being proven may be technically correct, the act of proving is a social act. The formal notation just makes this more precise than human language.

Retra 12y ago
Proof is "that which is convincing to a fair and rational mind." It should compel a rational actor into the verifiable mitigation of some risk. This particular fuss is one of the side effects of mathematicians' failing to properly adopt computers into their process. One of these days we will not accept a proof unless it is computer verified, and there will be no social aspect to it. It should not matter if your proof is 10,000 pages if a computer can follow it.
- lacker 12y ago
  It is still better to have a clean 1-page proof. There is no direct value for proving a theorem. Mathematics is nice because it's useful for further mathematics, useful for real-world applications, and beautiful. A 10,000 page proof that only a computer can follow is none of these things.
  - Retra 12y ago
    It is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms. So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
    - jackmaney 12y ago
      > surely there exist useful proofs that require 10,000 pages minimum The classification of finite simple groups "consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."[1] [1]: http://en.wikipedia.org/wiki/Classification_of_finite_simple_groups http://en.wikipedia.org/wiki/Classification_of_finite_simple...
      - Retra 12y ago
        That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. What you can't do is compress _all_ proofs to single-sentence proofs using a finite number of unique symbols.
- lotsofmangos 12y ago
  First of all you have to prove that a computer program is capable of verifying all unknown theorems correctly. This may be tricky.
  - mathattack 12y ago
    We know that a computer can't verify all unknowable theorems. (Theory of Computation) But perhaps one can verify all provable theorems. I suspect that computers will struggle on the cleverness factor, where proof requires joining multiple fields of math, rather than just running through algebraic manipulation.
    - lotsofmangos 12y ago
      But perhaps one can verify all provable theorems. Could a computer verify that the domino problem is undecidable? The proof consists of translating the problem into non-halting universal turing machines. http://en.wikipedia.org/wiki/Wang_tile#Domino_problem http://en.wikipedia.org/wiki/Wang_tile#Domino_problem

Retra 12y ago

Proof is "that which is convincing to a fair and rational mind." It should compel a rational actor into the verifiable mitigation of some risk. This particular fuss is one of the side effects of mathematicians' failing to properly adopt computers into their process. One of these days we will not accept a proof unless it is computer verified, and there will be no social aspect to it. It should not matter if your proof is 10,000 pages if a computer can follow it.

lacker 12y ago
It is still better to have a clean 1-page proof. There is no direct value for proving a theorem. Mathematics is nice because it's useful for further mathematics, useful for real-world applications, and beautiful. A 10,000 page proof that only a computer can follow is none of these things.
- Retra 12y ago
  It is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms. So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
  - jackmaney 12y ago
    > surely there exist useful proofs that require 10,000 pages minimum The classification of finite simple groups "consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."[1] [1]: http://en.wikipedia.org/wiki/Classification_of_finite_simple_groups http://en.wikipedia.org/wiki/Classification_of_finite_simple...
    - Retra 12y ago
      That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. What you can't do is compress _all_ proofs to single-sentence proofs using a finite number of unique symbols.
lotsofmangos 12y ago
First of all you have to prove that a computer program is capable of verifying all unknown theorems correctly. This may be tricky.
- mathattack 12y ago
  We know that a computer can't verify all unknowable theorems. (Theory of Computation) But perhaps one can verify all provable theorems. I suspect that computers will struggle on the cleverness factor, where proof requires joining multiple fields of math, rather than just running through algebraic manipulation.
  - lotsofmangos 12y ago
    But perhaps one can verify all provable theorems. Could a computer verify that the domino problem is undecidable? The proof consists of translating the problem into non-halting universal turing machines. http://en.wikipedia.org/wiki/Wang_tile#Domino_problem http://en.wikipedia.org/wiki/Wang_tile#Domino_problem