Timeline for What is the shortest program for which halting is unknown?
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 10, 2020 at 16:34 | comment | added | Jeremy Rouse | No, there are no natural numbers $a$, $b$ and $c$ for which $(a^{2} - 2) = (a+b)bc$. If one assumes that $a$ is minimal for which there exist such $b$ and $c$, then one can let $a_{1} = a - cb$, $b_{1} = (c+1)b - a$ and $c_{1} = c$. This triple also satisfies $(a_{1}^{2} - 2) = (a_{1}+b_{1})b_{1} c_{1}$. This gives a contradiction. (This is really a Vieta jumping argument like is used in the fairly well-known 1988 IMO problem. See here.) | |
| Jan 17, 2014 at 23:16 | comment | added | Thomas | Is the statement ∃a,b,c.a^2−2=(a+b)bc true? | |
| Jul 3, 2010 at 14:17 | comment | added | Andrej Bauer | This was some time ago. If I remember correctly we enumerated all universal statements up to 15 symbols where we took inequality is a basic symbol (and did not use negation). Approximately 3000 of those could not be recognized as decidable by our heuristics. Practically all of them were Diophantine equations (actually their negations), except possibly for a couple of systems of equations. We also investigated mixed-quantifier sentences and I think we got up to something like 10 and never found an interesting one. | |
| Jul 3, 2010 at 7:15 | comment | added | Daniel Litt | +1 I was wondering if someone would answer along these lines! Based on your blog post, I infer that you have not actually enumerated and solved all the statements shorter than the one you give; is that the case? | |
| Jul 3, 2010 at 6:22 | history | answered | Andrej Bauer | CC BY-SA 2.5 |