5 ms·

I don't know why you're being downvoted, but that is a perfectly valid statement. Everyone thinks proofs are this holy grail and totally rigorous, and they are

I don't know why you're being downvoted, but that is a perfectly valid statement. Everyone thinks proofs are this holy grail and totally rigorous, and they are on a certain level. But the idea is floating around that Mathematicians are infallible when in fact lots of proofs in highly complex areas of mathematics are NOT 100% perfectly rigorous. They contain a lot of skipping, because "it's trivial" and consensus. This approach may work very often, but there is a danger that sometimes it doesn't work and things get overlooked. Since mathematics is done in a bottom-up approach, at some point some fundament may or may not turn out to be wrong, which endangers parts built on top of it. The whole movement of rigorous automated proof systems is to prove mathematics from the very bottom to the very top in a 100% rigorous and verifiable way. Doing actual rigorous proofs a computer can verify is enormously tedious and many Mathematicians dislike it for that reason, because the inherently subjective "elegance" and "beauty" gets lost in translation.

zozbot234 4y ago
> because the inherently subjective "elegance" and "beauty" gets lost in translation. That's a very subjective POV, and perhaps one that varies by area of math. Many computer proof developments are more cleanly refactored/abstracted than the manual equivalent, because it's so easy to refactor a computer proof without worrying that the new proof might fail to prove the same statement.
q-big 4y ago
> Doing actual rigorous proofs a computer can verify is enormously tedious and many Mathematicians dislike it for that reason, because the inherently subjective "elegance" and "beauty" gets lost in translation. Couldn't we also interpret this fact that computerized proofs are currently often very unelegant as strong evidence that not a lot is understood about this topic and thus doing such "ugly" computerized proofs is the best we can (in most cases) currently do? Science at the boundary of human knowledge is often quite ugly; as our understanding of it grows, it often becomes more beautiful and elegant.
77pt77 4y ago
You should read "Proofs and Refutations by Imre Lakatos" if you haven't already.

zozbot234 4y ago

> because the inherently subjective "elegance" and "beauty" gets lost in translation. That's a very subjective POV, and perhaps one that varies by area of math. Many computer proof developments are more cleanly refactored/abstracted than the manual equivalent, because it's so easy to refactor a computer proof without worrying that the new proof might fail to prove the same statement.

q-big 4y ago

> Doing actual rigorous proofs a computer can verify is enormously tedious and many Mathematicians dislike it for that reason, because the inherently subjective "elegance" and "beauty" gets lost in translation. Couldn't we also interpret this fact that computerized proofs are currently often very unelegant as strong evidence that not a lot is understood about this topic and thus doing such "ugly" computerized proofs is the best we can (in most cases) currently do? Science at the boundary of human knowledge is often quite ugly; as our understanding of it grows, it often becomes more beautiful and elegant.

77pt77 4y ago

You should read "Proofs and Refutations by Imre Lakatos" if you haven't already.