UncombedCoconut

قبل سنتينdiscuss

Sadly, we can't, for such a test would already be enough to solve the halting problem: if a TM's status is provable, enumerate possible proofs (of halting and non-halting) until we find one and know the result; if the status is not provable, then the machine certainly cannot halt.

UncombedCoconut

قبل سنتينdiscuss

Mostly no: we did find some non-halting TMs that required new proofs, but none of those had the flavor of new math, per se. Indeed, we found that all but 30 of them could be proved by finite automata methods, meaning the TM's state/tape at any step could be reduced to one of finitely many states and we'd still know all we needed to know about future steps. I would argue that such a non-halting proof can't have much mathematical content. (Maybe a bit, in about the same way that an integer equation is sometimes proved unsolvable by considering it modulo n and checking every case.) Also, I learned some math I wasn't personally familiar with from the analysis of a particular machine: https://www.sligocki.com/2023/03/14/skelet-10.html (Zeckendorf's Theorem).

UncombedCoconut

قبل سنتينdiscuss

As a member of these chats: it's often like hitting on an idea on a break-room blackboard and working it out, except the interaction can be cited. That's a positive change, if we can follow through and add to the literature in due time. Here's hoping.

UncombedCoconut

قبل 3 سنواتdiscuss

This program is at least related to what you want: https://googology.fandom.com/wiki/Hypercalc -- and the community there has devised other systems for representing huge numbers with compact notations.

comments