It's the limitations for sure.

AI has dominion over the digital world, when it can verify things in Lean it's able to crush problems like they're a game of Go.

But when the real world and digital world don't quite connect AI is bottlenecked.