Hacker News
points by program_whiz 2 days ago | 0 comments
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.
[–] scarmig 1 day ago
I guarantee that you could not find a proof using brute force, even with literally trillions of dollars of compute. You're betraying a lack of understanding of the complexities involved, unless you're using a definition of "brute force" which is essentially equivalent to "intelligent search."
[–] jasomill 1 day ago
Brute force is certainly the wrong way to put it, but that doesn't mean it's easy to distinguish superhuman effort from superhuman intelligence, or, in the words of Thomas Edison, perspiration from inspiration.

Especially as the pure gruntwork involved in acquiring the knowledge required to merely understand the details of the mathematics involved represent at least a significant fraction of a human lifetime.

And unless this human process of knowledge acquisition continues, eventually no one will be left to understand and attach any significance to the results machines produce.

[–] skydhash 1 day ago
> 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.
[–] famouswaffles 1 day ago
>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.