4 ms·

"There is no permanent place for ugly mathematics" -G.H.Hardy I loathe these automatic proof systems (at least the state of the art today) - I think they may

"There is no permanent place for ugly mathematics" -G.H.Hardy I loathe these automatic proof systems (at least the state of the art today) - I think they may be useful for verifying that a complex CPU correctly implements integer arithmetic - but these proofs have little to offer a human mathematician. Let's follow Paul Erdos who said "one need not believe in god, but a mathematician should believe in The Book" The Book is where god (the supreme fascist) has collected the shortest and most elegant proofs in mathematics. Here's a great book written in this spirit (dedicated to Erdos) - http://books.google.com/books?id=KvQr9l0wgf8C http://books.google.com/books?id=KvQr9l0wgf8C when a theorem prover can produce a proof as elegant as as the one given in this book of say sperner's lemma then I'll give them another look. (No disrespect to Russell or the creators of these programs is intended, of course)

newt0311 18y ago
Agreed, partially. In mathematics, proofs really have two purposes. The foremost purpose is obviously to assert the logical necessity of the statement being proven. The second not so widely publicized purpose is to gain insight into mathematics. A proof is not just a way to prove that you are right. It is also a way to see what could be further explored. Thus the importance of elegance and insight in proofs. Automatic proof systems are great for the first purpose but they detract from the second. That is why they should not be considered the begin-all-end-all for mathematics. That is not to say that they are not useful or not an advancement. They are certainly that. Just that they are not a replacement for elegance.
yummyfajitas 18y ago
I don't agree. Lots of proofs are irreducibly ugly, even when the idea behind them is simple. Just too many edge cases and details. Automatic proof systems can avoid this. I think of it much like garbage collection and higher order functions. The machine code of a garbage collected program might be messier than a manually managed one. But python code is prettier than c code.
- kurtosis 18y ago
  you have strong point - i hadn't thought about it this way before. Just the other day someone called me out on a derivation and i spent a couple of hours writing out a very tedious proof. there were lots of special cases and i really resented the bastard when i was done. the experience was very much like filling out IRS forms. it would have been very nice to have a proof assistant to back up the points where i would have much preferred to handwave. I really like the comparison to manual memory management that's exactly what this proof felt like - freeing the mallocs. but think about the following two situations: (1) you have serious doubt as to whether a statement is true. presenting a proof removes all doubt. Computer proofs, no matter how ugly, are a win for this situation (2) you have overwhelming experimental evidence that something is true and you want a mathematical proof to help you understand why it is true. Computerized proofs are less helpful here - this is where you want an elegant and simple proof. it should be very intuitive how the result depends on the assumptions. it should be something you'll be able to remember when you're 70 years old.
  - yummyfajitas 18y ago
    I actually suspect the second situation won't happen for a long time. My guess is that we will instead have proof assistants. Basically, what will happen is that a human will come up with the big idea which motivates the proof, and will direct the proof assistant through the details. I'm thinking something along the lines of Isabelle or Coq + ProofGeneral, except of course much better.
    - ars 18y ago
      Or more along the lines of Computer Assisted Chess. A person assisted by a computer can play better chess than any human, and also better than any computer. Maybe it will be the same here.
- antiform 18y ago
  Proofs are almost never "irreducibly ugly." What has generally happened in the past is that mathematicians have abstracted the "ugly" parts of a proof, so that one only has to refer to a mathematical object (object in the OO sense). Ugly proofs for basic theory are usually the primary motivation for mathematicians to invent new mathematical abstractions. In fact, when some mathematician is said to have "reinvented a field of mathematics," it usually means that he has found a particular abstraction or perspective that allows for a simplification of the given field. In fact it happens in much the same fashion as you described. It's like writing a python port of a C program. You can abstract out the details until you have essentially reduced the proof to a chain of concepts.

newt0311 18y ago

Agreed, partially. In mathematics, proofs really have two purposes. The foremost purpose is obviously to assert the logical necessity of the statement being proven. The second not so widely publicized purpose is to gain insight into mathematics. A proof is not just a way to prove that you are right. It is also a way to see what could be further explored. Thus the importance of elegance and insight in proofs. Automatic proof systems are great for the first purpose but they detract from the second. That is why they should not be considered the begin-all-end-all for mathematics. That is not to say that they are not useful or not an advancement. They are certainly that. Just that they are not a replacement for elegance.

yummyfajitas 18y ago

I don't agree. Lots of proofs are irreducibly ugly, even when the idea behind them is simple. Just too many edge cases and details. Automatic proof systems can avoid this. I think of it much like garbage collection and higher order functions. The machine code of a garbage collected program might be messier than a manually managed one. But python code is prettier than c code.

kurtosis 18y ago
you have strong point - i hadn't thought about it this way before. Just the other day someone called me out on a derivation and i spent a couple of hours writing out a very tedious proof. there were lots of special cases and i really resented the bastard when i was done. the experience was very much like filling out IRS forms. it would have been very nice to have a proof assistant to back up the points where i would have much preferred to handwave. I really like the comparison to manual memory management that's exactly what this proof felt like - freeing the mallocs. but think about the following two situations: (1) you have serious doubt as to whether a statement is true. presenting a proof removes all doubt. Computer proofs, no matter how ugly, are a win for this situation (2) you have overwhelming experimental evidence that something is true and you want a mathematical proof to help you understand why it is true. Computerized proofs are less helpful here - this is where you want an elegant and simple proof. it should be very intuitive how the result depends on the assumptions. it should be something you'll be able to remember when you're 70 years old.
- yummyfajitas 18y ago
  I actually suspect the second situation won't happen for a long time. My guess is that we will instead have proof assistants. Basically, what will happen is that a human will come up with the big idea which motivates the proof, and will direct the proof assistant through the details. I'm thinking something along the lines of Isabelle or Coq + ProofGeneral, except of course much better.
  - ars 18y ago
    Or more along the lines of Computer Assisted Chess. A person assisted by a computer can play better chess than any human, and also better than any computer. Maybe it will be the same here.
antiform 18y ago
Proofs are almost never "irreducibly ugly." What has generally happened in the past is that mathematicians have abstracted the "ugly" parts of a proof, so that one only has to refer to a mathematical object (object in the OO sense). Ugly proofs for basic theory are usually the primary motivation for mathematicians to invent new mathematical abstractions. In fact, when some mathematician is said to have "reinvented a field of mathematics," it usually means that he has found a particular abstraction or perspective that allows for a simplification of the given field. In fact it happens in much the same fashion as you described. It's like writing a python port of a C program. You can abstract out the details until you have essentially reduced the proof to a chain of concepts.