I don't know much about Go but I'm guessing general proof automation would be many, many orders of magnitudes harder. The branching factor is huge (you can apply any theorem you want to the current goal and go down a bad path) and knowing if you're on the right track to finish a proof isn't obvious.