Shawn Ligocki, a Busy Beaver researcher, who writes about Turing machine champions, Collatz-like behavior, and the bbchallenge project.
Commenters call it a better source on actual Busy Beaver research than Aaronson's blog and praise its detailed explanations of hard machines.
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).
As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem was that the deciders and manual proofs were disorganized and somewhat suspect. The worst offenders here were Skelet #1, which needed a bespoke program to accelerate it to its ultimate pattern [0], and Skelet #17, which took Xu seven pages' worth of dense reasoning to prove non-halting [1]. The full Coq proof put a much-needed degree of confidence into these results.
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/184
See also this article (shared on Hacker News 2 weeks ago): https://www.sligocki.com//2023/10/16/bb-3-3-is-hard.html
Basically, they showed that a VERY small Turing Machine -- of a size many had hoped we would be able to exhaustively solve -- turns out to depend on whether something similar to the Collatz sequence ever haults.
In other words, research published just 2 weeks ago shows that we don't need a Turing machine with a couple thousand states to be beyond the reach of modern human mathematics -- even one with just a few states can stimy us.
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://bbchallenge.org/antihydra
I had no idea what this was talking about and followed links to a blog post that explained the first one ("Bigfoot"): https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html
This blog post made the "cryptids" make a lot more sense to me, so I thought I'd share that post here in case others were also wondering "what the **"
The “<A” notation indicates that the head of the Turing machine is positioned at the rightmost point to the left of the “<“, and is in state A. [0]
For instance, the notation `0^\inf 1^3 <B 0^2 1 0^\inf` is equivalent to `0^\inf 1 1 (B1) 0 0 1 0^\inf`.
[0] https://www.sligocki.com/2021/07/17/bb-collatz.html