今天最重的一条来自 OpenAI：他们声称用 AI 解出了纳维-斯托克斯方程的千年难题，并给出 Lean 语言形式化证明。如果独立验证能站住，这是非常大的事；但目前只有一篇官方博客，克雷数学研究所还没出现在任何声明里。
DeepMind 同天发布了 AlphaGenome Atlas，做的是另一件技术密度很高的事：把人类基因组全部 90 亿种单碱基变异的分子效应预测了一遍。今天这两条加在一起信息量不小，但都有各自的核查门槛。
OpenAI 声称提交纳维-斯托克斯方程 AI 解法，附 Lean 形式化证明
纳维-斯托克斯方程三维光滑解的存在性问题是克雷数学研究所七大千年难题之一，奖金百万美元。OpenAI 博客称已生成一份解法，并附上 Lean 语言写成的形式化证明。Lean 是证明辅助器，证明若能编译通过，至少在形式逻辑层面是自洽的，比纯叙述性论文多了一层机器可验证的约束——这一点不能不提，因为它给了外部数学家一个可以直接跑的文件，而不只是读一篇文章。
博客摘要没交代是哪个模型生成的、用了什么路径、形式化翻译经过了哪些步骤，也没提克雷研究所。目前只有 OpenAI 单方面声明，独立数学家的意见还没出来。形式化证明通过不等于数学社区认可——公理选取是否合理、形式翻译有没有遗漏，都需要专家逐步审查。这件事值得跟，但核查周期不会短。
来源：OpenAI Blog · On the Navier–Stokes Millennium Prize Problem
Google DeepMind 发布 AlphaGenome Atlas，覆盖全基因组 90 亿种单碱基变异
DeepMind 称 AlphaGenome Atlas 对人类基因组中约 90 亿种单碱基变异的分子效应做了预测图谱。这个覆盖量级对遗传病研究和药物靶点筛查有实用意义——大量临床相关变异在功能上仍是空白，批量预测能给研究者一个起点。
不过覆盖率和预测精度是两件事。摘要里没有出现独立基准测试数据，也没说具体预测了哪些分子表型（基因表达、染色质可及性，还是别的）。官方尚未说明版本细节。去读原文时，基准测试结果和预测类型是两个要先找的东西。
OpenAI 开放 500 万美元资助，方向是生成式 AI 对青少年的影响
OpenAI 宣布 500 万美元资助计划，支持研究生成式 AI 对青少年发展、身心健康与安全的影响，目前接受申请，强调支持独立研究。单笔规模和评审标准摘要里没有提。
OpenAI 在青少年使用 AI 的话题上一直面对监管和舆论压力，这笔资助出现在这个背景下，推动独立研究与做公关管理可以是同一件事。博客摘要没给出区分依据，读者自己掂量。有意申请的研究者可以去原文看细则。
来源：OpenAI Blog · Funding grants for new research into AI and teen development
—
来源
