Part of mathematics is formalization. There's no doubt that computers will help us with proofs more and more, but there's also the "discovering" of what statements we should be taking for granted. That involves things like intuition, insight, and intention. People didn't have a "least upper bound property" hundreds of years ago, even though they were studying the real numbers.

Just wanted to remind people that we haven't sucked the human element out of math.