0
Astra一次交出十项数学新结果：AI正在进入可验证的科研发现阶段
OpenAI内部版本Astra公布十项数学与理论计算机科学新结果，并同步交付论文、发现过程说明和Lean 4形式化证书。真正值得关注的不是“AI解出十道题”，而是一套人类选题、模型探索、形式系统验证、专家判断意义的科研生产流程正在形成。
标签: 数学研究
0
AI开始替数学家寻找反例：一个更适合机器的科研入口
AI参与数学研究的第一批规模化入口，未必是独立写出长篇证明，而是帮助研究者寻找反例、测试猜想、发现遗漏条件，并把候选结果交给Lean等形式化系统验证。
0
GPT-5.6补上凸优化30年缺口：论文、对话与Lean验证全部公开
加州大学伯克利分校研究者Phillip Kerger公布了一项无导数凸优化研究，将确定性精确函数值模型的查询复杂度下界从Ω(d)提高到Ω(d²/log d)，与1996年提出的近二次上界只差对数因子。