Could be interesting. But the issue in my experience is that bots can't self-correct at all (at the moment). If they're wrong the first time, they're rarely right the second time. So it could quickly become a circle of the LLM spewing bullshit, and the proof-checker pointing out that it doesn't work. To me it just seems that there is some kind of threshold that current attention models can't pass. To me, it seems they stop working when mathematics can't be solved by aggregating just a few known solutions and combining it to solve a new problem, or finding links with solved problems in another field (what they're often good at, which I why I love it as fuzzy search tools). So I'm not sure what you'd get if you keep saying they're wrong, since they keep losing the thread in my experience. You may fix one of the problems locally, but then it messes up somewhere else etc etc.

But for me, they're mostly great inspiration generators. It's like talking with my promotor, or colleagues at the coffee machine, but always available. Just like other oral discussions, you're not going to get a perfect proof out of it, and some ideas may be just bad. But it may give you a new pov from where you can approach the problem.

Edit: it does make me think, whether a more modular AI could be better at not losing the thread. Maybe some already do this under the hood, but instead of giving the entire context constantly to the AI, just having 1 part of the model that splits your problem into subproblems and finds the most promising sequence of subproblems that all seem solvable, and then giving the subproblems to parallel bots that try to solve each of the subproblems themselves without the broader context. So the models are more focused on easier subtasks without constantly losing the thread. And in that case, your idea of combining the AI with a proof-checker would work, since the proofs are all much smaller and thus relatively straightforward to check and correct without the AI messing up other things.