So, if you are going to refer to Godel's theorem, its best to explain your point. Godel's theorem is on of the most poorly understood popular ideas in mathemat

So, if you are going to refer to Godel's theorem, its best to explain your point. Godel's theorem is on of the most poorly understood popular ideas in mathematics and its easy to trip over (for you or the reader). I'm going to try to guess what you mean. You are trying to say that since a computer is essentially a formal system and humans are something more, we can't replace human mathematicians with computers to do the work because they won't be able to come up with new ideas outside a fixed problem space? In any event, I think you are misunderstanding @ihodes's question. The question is not "can we replace mathematicians with computers" but is more about the practice of mathematics. I.e., @ihodes is asking if the mental activity of experimenting and doing computations is conceptually similar to doing proofs.