Codex agent 把论文 RG 证明里的 10^-10^10017 优化到 0.00034

_onionesque · x · 2026-10-30

Scott N. Armstrong 分享了一个有趣的 agent 实战案例：其论文中的微扰 RG（重整化群）论证依赖某个指数参数「足够小」，他先让 Lean 形式化代码算出原条件小到 10^{-10^{10017}}——一个近乎荒谬的天文数字。随后他派出自己的 Codex agent（名为 dot）去优化这个界，agent 最终把它改进到 0.00034，并通过了新增约 100 万行 Lean 代码的形式化验证（其中包括 33×33 矩阵的 360 次幂等约 40 万行纯数值计算）。作者感慨 Lean 的妙处在于可以派 agent 进去「算数」：把形式化证明里模糊的定性条件变成具体可检验的数字。