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.
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.