Comment by 7373737373
2 days ago
Interesting new contender for simplest to state unsolved problem: The Antihydra
Does this program halt?
a = 8
b = 0
while b != -1:
if a % 2 == 0:
b += 2
else:
b -= 1
a += a//2
(// being integer division, equivalently a binary shift one to the right: >> 1)
Interesting, I hadn't heard this one.
I should see if I can model this in Isabelle or something and see what happens.
for reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/e...
Is that also the simplest unsolved state problem?
How does overflow behave?
It doesn't overflow.
Too bad, that makes it harder.
Fwiw, ChatGPT is able to say that it doesn't. I wonder what other classes of programs it's able to state if it halts?
Tom from the pub says that it does.
The math community surely expects a proof of that, and ChatGPT surely doesn't (yet) have one. (Maybe some day it will, as Kevin Buzzard and others are experimenting with asking language models to produce formal proofs.)
You could get LLMs to opine on many unresolved math conjectures, but I doubt much credence should be given to their responses, when not accompanied by a proof.
Most LLMs I've tried come up with invalid reasoning, many confuse empirical evidence (of simulating it for a few steps and it 'most probably not halting') with definite proof that it never does, some create invalid probabilistic mathematical arguments to the same effect
Others I've tried are caught in a loop of trying to prove the same, insufficient approach over and over again, lacking explorative and "creative" behavior
Generally it seems that LLMs lack the 'motivation' to actually try to solve unsolved problems especially if they know that they are unsolved or difficult
ChatGPT is able to say anything it wants. Surely you know this by now ...
What ChatGPT says has no relevance to whether it halts.