Skelet
Georgi Ivanov Georgiev (aka Skelet) was a Busy Beaver hunter who attempted to prove BB(5) in the early 2000s.
bbfind
In 2003, he announced his results on his webpage in which he shared his code bbfind (a 6000 line Pascal program) which he claimed enumerated 150M 5-state TMs and reduced them down to 164 holdouts (he called them "nonregular machines"). After manually analyzing these 164 nonregular machines he reduced it to 43 holdouts which he called "hardly nonregular" (HNR) which were not solvable by his program nor by hand. These 43 HNR TMs became famous examples of hard TMs to prove and these TMs began to be named by their place on this list (such as Skelet 1 and Skelet 17).
Due to the length and lack of comments in bbfind's source code, Skelet's work is not believed to have been independently verified.[1] It is now known that all 43 of these holdouts do not halt. Other work done in bbfind includes computing the correct value of BB(4) and for "RTM(5)" (the set of all "Reversal Turing Machines").
Skelet's 43 HNR TMs
- Skelet's original list: https://skelet.ludost.net/bb/nreg.html
- bbchallenge.org list: https://bbchallenge.org/skelet (canonically numbers the TMs)
- More info on some of Skelet's 43 TMs: https://discuss.bbchallenge.org/t/proving-bb-5-in-coq/225/6
TODO: Create a table for these holdouts
| Skelet # | Equivalent bbchallenge machine | Proof of nonhalting |
|---|---|---|
| 1 | ||
| 2 | ||
| 3 |