3 ms·

I disagree. Mathematics is often very ambiguous and formal proofs are often very long. The trick with informal mathematics is that the author and the reader (a)

by tel 13y ago

I disagree. Mathematics is often very ambiguous and formal proofs are often very long. The trick with informal mathematics is that the author and the reader (a) share a large amount of background and (b) tacitly assume that the text is talking about something interesting. So, given those things, you can usually resolve ambiguity by assuming that the proof is referring to the interesting part at hand instead of some boring detail. The downside to that is the ambiguity sometimes causes bugs. Formal proofs can be very long. It's an open problem today as to how to compress and decomplect them. It's extremely similar to the situation with programming. I'm not sure that I intend to refute your argument at its core—clarity does not imply great verbosity in my mind—but instead to color your example a little more. As a perhaps more specific, powerful example one could consider "Proofs by the Book" of Erdös-style wonderfully short proofs. These usually demonstrate the interesting characteristic of having very high "compression".

auvrw 13y ago
i half disagree. even informal proofs are often very long, but while they may omit some steps omitted, i wouldn't say they're ambiguous. it's just that writing something for a human who can (and in fact will find it easier to) fill in some blanks themselves is different for writing something for a machine, which only understands "how to do" kinds of descriptions. also, a tangent about Erdos: Erdos was really good at posing problems. if his proofs are concise, it could have something to do with the problems he chose to work on. i'm not saying there's no book, i'm just saying that the most perfect, concise proof of some facts might still turn out to be very long.
- tel 13y ago
  Certainly agree about Erdos/the Book. It's not an effort to prove that all elegant wonderful proofs are also concise, but instead that there exist elegant, wonderful, and concise proofs which are sometimes found. I always think of human proofs as the words on the page plus a significant guiding practice and convention of mathematics. Some proofs require more of that than others. Internalizing these proofs is highly non-mechanical. But I don't think we disagree here.

by tel 13y ago

auvrw 13y ago

i half disagree. even informal proofs are often very long, but while they may omit some steps omitted, i wouldn't say they're ambiguous. it's just that writing something for a human who can (and in fact will find it easier to) fill in some blanks themselves is different for writing something for a machine, which only understands "how to do" kinds of descriptions. also, a tangent about Erdos: Erdos was really good at posing problems. if his proofs are concise, it could have something to do with the problems he chose to work on. i'm not saying there's no book, i'm just saying that the most perfect, concise proof of some facts might still turn out to be very long.

tel 13y ago
Certainly agree about Erdos/the Book. It's not an effort to prove that all elegant wonderful proofs are also concise, but instead that there exist elegant, wonderful, and concise proofs which are sometimes found. I always think of human proofs as the words on the page plus a significant guiding practice and convention of mathematics. Some proofs require more of that than others. Internalizing these proofs is highly non-mechanical. But I don't think we disagree here.