没有墙 Math Inc. 的自动形式化代理 Gauss 在短短 3 周内完成了“强素数定理”项目——这是一个连 Terence Tao 和 Alex Kontorovich 都花费了超过 18 个月却陷入困境的任务。 “我们正进入一个黄金时代，任何人都可以召唤人工数学家进行研究。随着经过验证的数学成为 AI 的训练场，我们正在创造超越人类局限性的机器普遍主义者——数字时代的冯·诺依曼。”