谷歌 DeepMind 开发的一个基于 Gemini 的智能体，在 BB(6) 问题中为 11 台停机状态未知的图灵机发现了新的加速规则。

打开网易新闻 查看精彩图片

这些规则随后在 Lean 中完成了形式化证明，相关图灵机被归类为 Cryptids。

换句话说，AI 不只是解题，还自己找到了值得证明的命题，并把证明写到了可被机器检验的程度。