During a visit to Germany, Ligocki’s encounter with Marxen over beers led to a revival of the closed tape language method, a powerful tool in the Busy Beaver Challenge. Team efforts cracked the challenging machines Skelet #1 and #17, with new contributors refining proofs. An amateur mathematician, Kądziołka, introduced Coq software for mathematical proofs, raising the rigor of the project. With mxdys’ remarkable contribution, they finally proved that the machine discovered by Marxen and Buntrock was the fifth busy beaver. However, the discovery of the Antihydra machine in BB(6) poses a new, formidable challenge. Contrary to popular belief, the BB Challenge may hold surprises beyond our expectations.
https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/