程序员和业余数学家证明忙碌海狸数 BB(5)

文章预览

匈牙利数学家 Tibor Radó 在大学期间主修的是土木工程，一次世界大战中断了他的学业，他被派往前线，被俄罗斯俘获送到了西伯利亚的劳改营，在狱友的指导下学习数学。四年后他成功逃狱，穿越北极数千英里返回了祖国，重新回到学校。他在 1920 年代发表了数十篇数学论文，1930 年接受了俄亥俄州立大学的教职，任职达 35 年。他在晚年对图灵停机问题进行了提炼，1962 年在一篇论文里将重新表述的图灵停机问题称之为忙碌海狸游戏。忙碌海狸数通常用 BB(n)表示，它是一个快速增长的大数。现在程序员和业余数学家合作，使用形式化证明工具 Coq 证明 BB(5)=47,176,870。BB(6)需要证明 Collatz 猜想（Collatz conjecture），短期内难以突破。 https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-t ………………………………