> Roger Penrose argues that human intelligence can't be a computation because we can arrive at true conclusions even though they are not formally provable.

Tarski proved that it's impossible to prove truth within the same system anyway, so this isn't a strong objection and is in fact subtly incorrect. Humans don't arrive at "true" conclusions either, we just fail to find contradictions and call it good enough.

Probabilistic reasoning is just as powerful in practice as tractable computations.