James Buddenhagen wrote:
. . . something that has been bothering me for a long time: when should I accept that something is true?
It's always been true that you had to trust your own brain, that it hadn't been fooled. A proof is just an argument that's supposed to be convincing, that hopefully gets you a lot closer to believing. Math proofs convinced in a way that was (still can be) so impressive that it seemed to transcend human limitation. But proofs always run on a substrate. Nobody mentioned truly formalizing math and using proof- checking programs. Doing that would break the problem down. 1) Most proofs aren't perfectly formal. Someone would have to fill in the tedious gaps, and yet, 2) You want at least the statement of what is proven to be still human readable, because unless you think you know what is claimed, what good is a proof? 3) The proof-checker should be a simple program, easy enough for many people to understand in detail, and many many people to understand in principle. It should be compilable and runnable on anybody's computer. 4) Once you're convinced you know what it says and that it's true, you still have to worry about what it means. Consider all the baloney smart people say about Goedel's proof. I couldn't remember what it means exactly or how it works, a month after reading GEB. I think if such a movement could get started, it would fuel itself, as a huge backlog of proofs were debugged. Enough evidence of sloppiness and interesting questions and there would be a moral momentum. I think this would air out some of the psychological, sociological or institutional problems others have mentioned here. It wouldn't be so easy to mystify, or to brush over things. I'm still stirred by Leibniz's nutty "Calculemus!" ideal: "For it would suffice to take their pencils in their hands, and say to each other: Let us calculate." http://www.tiac.net/~sw/2003/08/calculemus.html On the other hand it could reduce the pressure to make proofs clear to humans ("Just run the checker!"). Item 2 above amounts to a user-interface or programming-language design problem. I would like to see usability engineers, especially, critiquing math. For use by other mathematicians, mainly. --Steve