The discussion here is talking about helping individual research with proposals a human will read. 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. There is no "automatic verification" of a system design proposal, and no way to figure out from 10s of millions of proposals which is best automatically, and also assuming people in this discussion don't have 10s of millions of dollars to throw at every design problem.