Given a formal theory, there is no fundamental barrier to emitting only sentence prefixes that do have a continuation into a provable sentence of that theory. There is a random algorithm that can produce any provable sentence of a theory in this manner.
Note that this is very different from (and does not require solving) the generally undecidable problem “given an arbitrary prefix, determine whether it can be continued into a provable sentence”.
Current LLM architectures can’t implement such an algorithm directly, but in principle could do so with some sort of unbounded “scratchpad”, just as humans would also require some form of unbounded external storage to implement such a process.
Given a formal theory, there is no fundamental barrier to emitting only sentence prefixes that do have a continuation into a provable sentence of that theory. There is a random algorithm that can produce any provable sentence of a theory in this manner.
Note that this is very different from (and does not require solving) the generally undecidable problem “given an arbitrary prefix, determine whether it can be continued into a provable sentence”.
Current LLM architectures can’t implement such an algorithm directly, but in principle could do so with some sort of unbounded “scratchpad”, just as humans would also require some form of unbounded external storage to implement such a process.