0
1万名AI智能体、88小时与一道世纪难题：怎样理解Navier–Stokes方程突破
OpenAI公开三维不可压缩Navier–Stokes方程反例及Lean形式化版本。本文解释它解决了什么、平滑外力为何符合官方命题、多智能体与形式化验证各自扮演什么角色，以及优先权和算力集中带来的新问题。
标签: Lean
0
AI开始替数学家寻找反例：一个更适合机器的科研入口
AI参与数学研究的第一批规模化入口，未必是独立写出长篇证明，而是帮助研究者寻找反例、测试猜想、发现遗漏条件，并把候选结果交给Lean等形式化系统验证。
0
GPT-5.6补上凸优化30年缺口：论文、对话与Lean验证全部公开
加州大学伯克利分校研究者Phillip Kerger公布了一项无导数凸优化研究，将确定性精确函数值模型的查询复杂度下界从Ω(d)提高到Ω(d²/log d)，与1996年提出的近二次上界只差对数因子。