3 ms·
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:
by 7373737373 1y 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)
https://www.sligocki.com/2024/07/06/bb-6-2-is-hard.html https://www.sligocki.com/2024/07/06/bb-6-2-is-hard.html
https://bbchallenge.org/antihydra https://bbchallenge.org/antihydra
- tombert 1y agoInteresting, I hadn't heard this one. I should see if I can model this in Isabelle or something and see what happens.
- 7373737373 1y agofor reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/eda179635c14c1c9a0abb51843cd40e291b5c70b/FormalConjectures/Other/BeaverMathOlympiad.lean#L92 https://github.com/google-deepmind/formal-conjectures/blob/e...
- gowld 1y agoIs that also the simplest unsolved state problem?
- fragmede 1y agoFwiw, ChatGPT is able to say that it doesn't. I wonder what other classes of programs it's able to state if it halts?
- schoen 1y agoThe 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.
- SirChud 1y agoWhat ChatGPT says has no relevance to whether it halts.
- IshKebab 1y agoChatGPT is able to say anything it wants. Surely you know this by now ...
- 7373737373 1y agoMost 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
- yifanl 1y agoTom from the pub says that it does.
- ygritte 1y agoHow does overflow behave?