Hacker News
points by skydhash 1 day ago | 0 comments
> 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.

[–] QuesnayJr 1 day ago
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.
[–] jasomill 1 day ago
This is trivially true for any theorem with a proof that can be automatically verified in finite time, but does not preclude the universe lacking a suitable combination of monkeys, typewriters, and time to do so.
Hacker News