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.
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.
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.