AI 编程实时动态与要闻

2026-11-06，Physical Superintelligence（PSI，@psipbc）宣布：其内部研究系统在非公开 Anthropic 模型实例上，于第三天得到 Aaronson–Ambainis 猜想（2008 年起开放）的完整证明，并经 Lean 接受；随后又改进两次。官方研究页与 GitHub Lean 4 形式化仓库已公开。厂商口径尚无期刊同行评审；README 仍要求人工核对形式化陈述与原猜想是否一致。

查看大图

针对大模型数学证明缺乏步骤级验证标签与上下文精确复制存在 LM Head 梯度瓶颈的两大难题，今日两项基础研究给出突破：NYU/UCLA/Stanford 联合推出 LeanPRM（arXiv:2610.17697），利用 Lean 4 证明助手自动构建含 10,634 篇证明与 15.2 万个步骤标签的零人工标注数据集，将 Qwen3-4B 步骤验证准确率从 48.2% 拉升至 74.7%（远超 PRM800K 的 60.3%）；康奈尔大学提出复制粘贴语言模型 CPLM（arXiv:2610.19247），以仅约 3% 算力开销打破 LM Head 梯度瓶颈，使窗口仅 w=128 的滑窗模型追平全注意力困惑度并在 4 倍外推长度（16K）持续收益。

查看大图

纽约大学（NYU）联合 Google DeepMind 杰出科学家 Rémi Munos 等在 Hugging Face 与 ArXiv 正式公开了《Learning to Discover Interesting Mathematics》（arXiv: 2609.28603）。随着大语言模型在形式化数学证明（Lean 4、Mathlib）中展现出强悍的求解能力，AI 已经能够轻易生成成千上万个冷僻枯燥的平凡定理，但大模型究竟能否自主识别出“真正有学术价值且有趣的数学新知”始终未解。团队首创以“证明长度与命题表述长度之比”作为定理内在趣味性的量化指标，并训练了 27B 参数的证明难度预测模型，使系统能够在无人预设目标的情况下，自主猜想、筛选高价值定理并自我扩建形式化数学知识库。

查看大图