It will cook only as long as brute force through search space is cheap and economically viable.
Yep, that's how Euler, Gôdel, etc. proved their theorems, both easy and difficult ones.
They trawled through the search space just like a swarm of 10000 agents.
And there are so many indicators that it's not currently economically viable and will only be if retail price is massively increased and strong regulatory barriers to competitors are erected. ;)
Hard numbers would be proof, love... not indicators.
Yes, AI can explore thousands of ideas at once, no, that's not "brute forcing the search space" because the search space is way larger than you think it is.
Godel, Euler, Ramanujam, etc. didn't burn millions of dollars or drudged through search space like OpenAI's agent do to prove what they need.
Let's not forget using Lean as a crutch throughout the way rather than as a final tool for formalization and verification.