>> Almost certainly. If it really is smarter-than-human - say, twice as >> smart as I am - then just the fact that it's running in a Turing >> formalism should be enough for it to deduce that it's in a simulation.
This is very well put. I had the same objection and you've captured it perfectly.
I think the original remark misses the depth of Church-Turing. It's not just talking about what you can do with a computer, it's talking about what you can do with _any conceivable_ formal system. If you can find expressible regularities in the universe which can't be described under the lambda calculus then you've disproven the conjecture.