alt Hacker News> 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
It’s kinda like the project where someone generated a lot of midi files for all possible pop riffs to copyright them. If you have a start and endpoint, rules for navigation, and unlimited computes, you can brute force anything. The nice stuff is when you made exploration efficient.
Other than for maybe Navier-Stokes, they just didn't brute force it in the way you guys are thinking. Most unsolved math problems are not susceptible to brute force, which is why the problems remained unsolved. AI is so quick it can of course try more ideas than a person, but each idea is executed at genius IQ level. Even if you knew the broad outlines of the proof of quasi-Riemann, there are probably only 20 people in the world who could have executed it.