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

  匈牙利数学家 Tibor Radó 在大学期间主修的是土木工程,一次世界大战中断了他的学业,他被派往前线,被俄罗斯俘获送到了西伯利亚的劳改营,在狱友的指导下学习数学。

  四年后他成功逃狱,穿越北极数千英里返回了祖国,重新回到学校。他在 1920 年代发表了数十篇数学论文,1930 年接受了俄亥俄州立大学的教职,任职达 35 年。他在晚年对图灵停机问题进行了提炼,1962 年在一篇论文里将重新表述的图灵停机问题称之为忙碌海狸游戏。忙碌海狸数通常用 BB (n)表示,它是一个快速增长的大数。现在程序员和业余数学家合作,使用形式化证明工具 Coq 证明 BB (5)=47,176,870。BB (6) 需要证明 Collatz 猜想(Collatz conjecture),短期内难以突破。