> The frustration, for Hamkins, goes beyond mere incorrectness—it’s the nature of the interaction itself that proves problematic. I would assume pairing LLMs with a formal proof system would help a lot. At the very least, the system can know what is incorrect, without lengthy debates, which frustrate him most. This won't help the system discover or solve new math, but it make the experience far more endurable.
That itself may be tricky. Suppose you proof system tells that the proof is correct — how do you verify it is proof of the assertion you want, unless you have beforehand written the "test harness" by hand?
At least in programming, formally checking that the code does exactly what is required is orders of magnitude harder than simply writing code that compiles.