>That is different from spending 10s of millions to do a brute-force search of lots of different proofs which can be verified by LEAN automatically.

That is not remotely how the vast majority of the proofs have worked. You don't know what you're talking about, but that seems par the course for these discussions.