IME, LLMs are primarily good at grinding through cases, which is why you see them pushing upper and lower bounds and finding counter examples.

I spent a few weeks working on a number theory proof with Claude off and on and it spent hours and hours and hours grinding through one shape of polynomial after another, reporting "progress", and it's true, it proved what I was trying to prove for more and more classes of polynomials, but it was biting off pieces of an infinite tower of classes with no hope of closing it for _all_ polynomials.

That happens to be a good way to find counter-examples, though, and when I posed a slightly different version of my problem, it found a counter example in about 90 minutes.

And in fact, finding the counter example for the related problem allowed Claude to finally prove the thing I wanted to prove to begin with, by lifting the problem to a characteristic where that counter example didn't exist, proving my question there, and then proving that it still was equivalent to my original question.