每天听简报，了解最新科技、AI、软件资讯
OpenAI 刚发了一份关于 Navier-Stokes 方程的证明，同时挂上了 Lean 4 的形式化版本。John Cook 说，大家在吵方程本身，他更在意这件事：可机器验证的证明以前贵得吓人。两千零五年有人估过，本科教材一页大约要四十个工时。研究论文更密，按二十倍算，一百六十六页得十三万小时。OpenAI 这边用 Lean 验证只花了十七小时。他把成本砍了四个数量级，叫革命都不夸张。形式化不只服务数学，安全策略能不能自洽、智能合约赔付上限、关键算法对不对，这些都比研究论文好算账。他自己用 AI 给博客核对过证明，以前请人干一周的活，现在才敢自己做。
进度保存在本设备 · 登录同步