[bubblyworld]

Indeed, proof-checking tools like Lean can reason about their own logical systems and prove their own incompleteness, but I doubt Penrose would conclude that they are not formal systems as a result.

I like to think people can still make progress on questions of intelligence and consciousness though. Michael Levin's work comes to mind, for instance. Science is just at very early stages of understanding =)