Gemini智能体自主发现并形式化验证BB(6)中11台图灵机的新加速规则

Marco Dos Santos、Satinder Singh、Tom Zahavy等研究者在arXiv发表论文称，他们构建的基于Gemini的智能体流水线，把模式识别、自动猜想、非形式化数学推理与Lean形式化证明整合在一起，用于自动发现图灵机的“加速规则”，即概括大量执行步骤的紧凑数学规则。该系统自主发现并形式化验证了“忙碌海狸”BB(6)中11台机器的新型类Collatz加速规则。作者暂将这些机器归为“Cryptids”：它们从空白纸带开始的执行过程已有精确的紧凑数学描述，但是否停机仍未解决。作者表示，这一归类尚待社区认可。