If it's just all symbols then computers should be better at it than us. The reason we can prove deep theorems by choosing the right path through an impossibly large combinatorial space is because we perceive structure and meaning, and we use that to guide us. We gaim an intuition for something that's "going on underneath" and so don't just perform random searches.

Explaining simple proofs to students often leaves them feeling that they've followed the steps, but don't undertand. There is more than just symbols.

Humans have a lot more bandwidth and computational power than you might think. And the search space for most proofs is not all that large compared to say a go board once you consider how many different proofs also work.

PS: 1-10 petaflops by some estimates, just not that many significant digits per calculation.

When you say `most proofs' do you mean proofs that you would find in an intro level course, or do you something more. I strongly disagree that the search space for most proofs is as small as go. This may be true once you restrict to a suitably relevant field, but this is a nontrivial reduction which takes a great deal of insight!

Fermat's last theorem resisted the attempts of mathematicians for three hundred years because it required insights so complex they couldn't be formulated without a deep understanding of disparate subfields.

To tie this back to the go analogy, the search space of go is large because the branching factor is big (<400) and because the number of moves is quite large (<400 as well, for all but a very few bizarre situations). For real proofs, while the branching factor may be substantially smaller (given some axiomatic system), the length of the proof is much much longer. The exponent in proofs beat the branching factor of go.

Interesting take. Could you comment on my sibling comment?(Here: http://news.ycombinator.com/item?id=4106554 )