[sfink]

Perhaps an LLM could produce a plausible-looking proof that is completely and utterly incorrect.

As a party trick.

[generalizations]

Wouldn't that be the point of pairing it with Lean? You wouldn't get false positives.

[Sharlin]

Doesn’t mean you’d get true positives either. Garbage in, garbage out.

[akoboldfrying]

IIUC, any sensible way of "pairing up" these things will mean that anything you get out will be true. But the search might take millennia, and the outcome might be nothing (equivalently, "the LLM's conjecture is false").

[hackerlight]

This is equivalent to saying it's not going to work.