It arguably matters a lot less in this context - you don't need experience to see when Copilot has failed at Lean, the compiler will tell you anyway. But I'm no

It arguably matters a lot less in this context - you don't need experience to see when Copilot has failed at Lean, the compiler will tell you anyway. But I'm not saying that understanding it yourself won't matter. In fact, I wouldn't be surprised if the gap between him and more mortal mathematicians actually widens with the availability of those tools.