>but at the end of the day if you really want to precisely say what it is you're talking about, it's symbols
Hear hear! I'd go one step further and say its ALL symbols. Any associated real-life meanings that help a human intuitively understand the equation is purely coincidental and actually a distraction. I've repeated this argument ad-nauseam : http://news.ycombinator.com/item?id=4085558
Don't know who it was ( Martin Gardner ? ) who once said three dinosaur plus two dinosaur is still five dinosaur. The implication is that symbol pushing and symbol manipulation is way more fundamental than having humans around who can associate three and two with human artifacts and then add them to satisfy their intuition. The dinos will add up to 5 regardless of the human intuition.
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.
Hear hear! I'd go one step further and say its ALL symbols. Any associated real-life meanings that help a human intuitively understand the equation is purely coincidental and actually a distraction. I've repeated this argument ad-nauseam : http://news.ycombinator.com/item?id=4085558
Don't know who it was ( Martin Gardner ? ) who once said three dinosaur plus two dinosaur is still five dinosaur. The implication is that symbol pushing and symbol manipulation is way more fundamental than having humans around who can associate three and two with human artifacts and then add them to satisfy their intuition. The dinos will add up to 5 regardless of the human intuition.