> Separately, the halting problem would not apply in the first place.
The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result.
> The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ...
Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.
> ... and the LLM is back at trying to create a program which is feasibly provable.
No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result.
> The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ...
Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.
> ... and the LLM is back at trying to create a program which is feasibly provable.
No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.