Mathematical Conversations
What persuades us to accept a proof as correct, and can computer learning help us in that?
Undergraduate mathematicians are taught Hilbert's dream that theorems should be built up from a solid axiomatic base, and that the whole structure of mathematics is (or should be) a solid verifiable whole. However, this is rather far from how mathematicians really study proofs. Rather than verified as being rigorous from first principles, researchers typically examine proofs in the light of their own experiences, knowledge and understanding, and believe them to be correct when they fit, as if they belong, into a complicated web of ideas. This approach has its evident dangers but has served the mathematical community well. Now computer software is being developed that supposedly will fulfill the undergraduate dream of objectively verifying proofs back to first principles. Is this useful? Will we be more certain that our theorems are true as claimed? Will this serve the development of our mathematical understanding?