Pavel discovered a 3-state 4-symbol TM that can compute an Ackermann-level function and halts with a large number of non-zero symbols on the tape. The TM can be approximated as BB(3,4) > Ack(14). This TM is the first in the wild to simulate an Ackermann-level function. Pavel’s code specified the result as Halt(SuperPowers(13)). The validation process using “Inductive Proof Validator” yielded precise values for the tape symbols. The TM’s behavior is described by a double induction rule. Surprisingly, the TM does not contain Collatz-like rules, hinting at potentially undiscovered Ackermann-level TMs with such rules.
https://www.sligocki.com//2024/05/22/bb-3-4-a14.html