Here's another way to look at it: we all know people who could ace their high school math tests because they had memorized the rules of manipulation but weren't good at math--as evidenced by their poor performance in college and failure to succeed in future STEM classes. If "the symbols and their manipulations are what you're studying" (which, I agree, there is some truth to), then what is it exactly that these people were lacking?
(BTW, an inconsistent set of rules would correspond to a version of DragonBox where there was a cheat code you could enter, and then easily solve every problem. So it would not "work just as well", and this would be pretty clear to a cheating gamer.)
But which algebra, and which rules ? There are infinitely many algebras ( eg. Algebra over the field of reals, Banach Algebra, relational algebra, boolean algebra, sigma algebra etc. ) The "rules" are really constructs you decide that apply to the elements of the space that conform to your algebra. So for example the reals are a field that have ordering, so you can talk about less than and greater than, but the complex numbers don't have an imposed order and you'd have to first define a norm to map them onto the reals. The AltDragonBox with its own inconsistent arbitrary rules will still have some algebraic encoding. Whether that's useful to you is debatable. Like in my algebra I could overload plus to mean multiply and square root to mean divide by 7 and add -3 and then try to figure out what exponentiation works out to. It would be interesting...maybe not useful, but its still an algebra. Maybe you won't have closure...the elements may not end up in a field or even in a semigroup...its a nice make-believe algebra.
AltDragonBox could be exactly that -- day and night cancel, except for symbols when its constellation is rising, in which case they divide, except for odd numbered Fridays in a leap year. Oh, and do it with numbers instead of day/night symbols.
A lot of the time though, the other rules for alternative algebras produce very dull and boring algebras.
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.
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.
PS: 1-10 petaflops by some estimates, just not that many significant digits per calculation.
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.