alt Hacker NewsUsing LLMs to generate piles of code and/or proofs of dubious quality is very questionable thing, and I understand these non-stop debates about it.
But in this case, as using plain brute force is already quite a common thing in searching for counterexamples, using LLMs as a sort of more advanced brute force seems to be just the right thing to do, so I struggle to understand so much hostility to this approach.
Replies
The good thing about math is that you can formally verify the results, making hallucinations much less scary.
This is similar to games, where large learning models had some of their first big wins (go). Games, like math, have strict rules that can be used to prune invalid outputs.
It is already in the making, the next big step in math will be the complete formalization of all existing, relevant theorems and proofs via LLMs.
Without seeing the Fable trace that produced this, claiming it amounts to ‘advanced brute force’ seems like a leap.
> I struggle to understand so much hostility to this approach.
It's going to be really rough for a lot of folks as machines get better and better at domains that the human brain was exclusively useful for. I tend to view the hostility as a mix of both "unless we have proof this could all be hokum" and "we're going to lose a lot of what we consider makes humans amazing".
Compassion is going to be very, very important in the next few years. We're going to hurt, both internally and externally.