Skelet

Georgi Ivanov Georgiev (aka Skelet) was a Busy Beaver hunter who attempted to prove BB(5) in the early 2000s. 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 there place on this list (such as Skelet 1, Skelet 17 and Skelet 34).

Due to the length and lack of comments in bbfind's source code, Skelet's work is not believed to have been independently verified. 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").

bbfind

See https://skelet.ludost.net/bb/

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