That's just wrong. Hofstadter never says that theorem proving is mechanical, and if he did, he'd be wrong. Demonstrating a proof can be mechanical, which is w

That's just wrong. Hofstadter never says that theorem proving is mechanical, and if he did, he'd be wrong. Demonstrating a proof can be mechanical, which is why proof assistants such as Coq can work, but finding a proof, that's an art.