数学同行筹备新期刊:以理解优先于首发、Lean 形式化验证保障严谨性
数学研究者 Shaoming Guo 等在 Terence Tao 博客宣布正筹备一本新期刊,拟以“理解优先于首发”和“论文证明须经 Lean 形式化验证”为核心准则,以应对大语言模型参与数学证明后难以察觉的错误风险。该刊尚在规划阶段,除开放获取等传统价值外另设上述两条标准,作者同时公开征集对这一方案及不同期刊愿景的反馈。
按时间排列的全部内容。默认只显示通过双重评分的入选条目;切换到“全部收录”可以检索所有抓到的资料。
160 条收录动态,更新于 09:40
全部收录包含没有通过评分的资料,标题以常规字体显示并标为“未入选”,只供检索,不写入选理由。
数学研究者 Shaoming Guo 等在 Terence Tao 博客宣布正筹备一本新期刊,拟以“理解优先于首发”和“论文证明须经 Lean 形式化验证”为核心准则,以应对大语言模型参与数学证明后难以察觉的错误风险。该刊尚在规划阶段,除开放获取等传统价值外另设上述两条标准,作者同时公开征集对这一方案及不同期刊愿景的反馈。
Francesco Maggi 在 Terence Tao 博客客座文章中提出,LLM 已能生成数学证明,如带强迫项的 Navier–Stokes 方程有限时间爆破解构造和准黎曼假设证明提案,但需数学界持续独立审视。
2026年10月18日一周热闻回顾:多伦多大学终身荣誉教授李仁科10月10日在西安出席学术会议期间辞世,享年65岁;清华大学朱军、甘霖等6人获2026年度“CCF青年科技奖”。励建书与王坚10月14日在第六届智能计算创新论坛上共同启动“未来数学计划”,聚焦AI与数学双向赋能。
在第六届智能计算创新论坛上,中国科学院院士励建书提出,AI赋能下数学研究范式可能改变,单纯为发表论文的研究价值将大幅下降,对顶尖数学家的需求会大大增加。他倡导启动“未来数学计划”,建立完全开放、不依赖单一公司的“AI+数学”创新共同体。他还指出Math for AI的数学基础研究仍滞后,AI目前主要靠工程师推动。
研究团队发布技术报告,介绍跨会话持续运行的自主研究智能体 Épi,它结合分层记忆、版本化分支和独立评审,在固定验证规则下产出 120 项纪录结果,包括 20 项数值界纪录和 100 项构造纪录,其中 n-queens 常数区间收窄约 84 倍,四次 Feigenbaum 吸引子维数的严格区间收窄超过 360 万倍。
入选理由作者团队公开了可核查的构造与证书,研究者能据此判断自主研究智能体在数学与算法设计上已能产出何种可检验结果。
据 Scientific American 报道,多组数学专家认为 OpenAI 9 月初公布的 166 页 Navier-Stokes 问题潜在解法与西班牙数学家 Diego Córdoba 和 Luis Martínez-Zoroa 的方法只是表面相似,EPFL 数学家 Gonzalo Cao-Labora 称细节上是另一套方法。
Anthropic 发布博文称,其内部研究用 Claude 模型用不到 30 分钟追溯出五条 NIST 标准椭圆曲线(P-192、P-224、P-256、P-384、P-521)的种子来源,为一桩延续约 26 年的密码学悬案提供了可复现的答案。
Claude 在不到 30 分钟内解开了一个困扰 25 年的密码学谜题。 有一大类研究问题,其搜索空间极其庞大,但验证成本很低。 AI 智能体可以大规模探索假设、运行实验并做出新发现。我们将看到更多这样的案例。
SAIR Open Math OS 已软启动,提供类似前沿 AI 模型的网页界面与服务,目前托管 DeepSeek V4.1 Flash、Kimi K3 和 GLM 5.3 Flash 等开放数学模型,能力大致落后当前前沿模型一年左右,无法完成“一次性解题”,但可用于中等规模 Lean 形式化、总结或讨论数学论证与主题。
Jeremy Avigad、Kevin Buzzard、Johan Commelin 等七位作者在 Kevin Buzzard 博客发文《How to Formalize All of Mathematics》,回应近期自动形式化全部数学文献的提案。文章指出形式数学与 informal 数学面临平行的问题,核心在于优先产出时速度、规模与理解之间的权衡,全文主要围绕这一权衡展开。
北京大学董彬在2026未来科学·创想季活动上表示,AI对数学的冲击已是"房间里的大象",OpenAI一次性公开722篇数学手稿后已有3篇因错误被撤回。他牵头的AI4MATH团队今年4月研发的Rethlas-Archon在全自动条件下用近两万行Lean 4代码否定了悬置十余年的安德森猜想,获Nature专题报道。他认为数学家应拥抱AI,企业侧重模型训练、高校提供高质量数据与评测问题。
10月14日,在Science/AAAS与之江实验室共同举办的第六届智能计算创新论坛上,中国科学院院士励建书与中国工程院院士王坚共同启动“未来数学计划”。该计划围绕AI与数学双向赋能,重点开展四方面开放创新:研发数学基础模型、开展形式化验证研究、研究AI背后的数学机理、推动数学基础能力赋能其他学科。
科学网文章梳理2026年AI对数学研究的冲击:OpenAI于9月8日称其未公开模型调动约一万个智能体、用88小时生成纳维-斯托克斯方程存在性与光滑性问题的证明手稿,10月6日又在GitHub公开722篇内部前沿模型生成的数学手稿,覆盖数论、几何、代数等17个领域,次日因一处符号错误撤回3篇涉及霍奇猜想的手稿,手稿总数降至719篇。
Anthropic 称,一名员工让内部研究模型 Claude 在不提供线索的情况下追查 NIST 椭圆曲线种子来源,Claude 在不到半小时内查明 P-192。
入选理由NIST 椭圆曲线种子来源这一长期悬案被 Claude 在半小时内解开,密码学与数学研究者可据此复核并复现。
Anthropic 用自然语言规格和自动评分器让 Claude 在闭环中设计量子电路,在化学、优化、量子模拟、数论和数值计算共八项任务上给出比已发表最优方案使用更少量子比特和门的新设计,部分提升达一个数量级以上。
入选理由Anthropic 让 Claude 在闭环中自主设计量子电路,八项任务均优于已发表设计,为量子算法资源估算提供了可复用的自动化路径。
Anthropic 宣布投入 500 万美元的资金、算力和 Claude 使用权限,与 Simons Foundation 合作支持数学界应对 AI 带来的变化。
How can the math community forge the best path forward in the AI age? We're committing $15M to workshops and initiatives — plus free AI computing resources for foundation-supported researchers — through new partnerships with @AnthropicAI and @OpenAI: https://bit.ly/4zpfIbW #math #science #AI
@Google - 排行榜:https://arcprize.org/leaderboard - 复现公开结果:https://github.com/arcprize/arc-agi-benchmarking - 测试政策:https://arcprize.org/policy - Gemini 4 Argon 完整结果:https://arcprize.org/results/google-gemini-4-argon
Simons Foundation 启动一项 1500 万美元的计划,用于评审 OpenAI 的研究成果、学习 AI 工具以及制定 AI 使用的集体标准,OpenAI 和 Anthropic 也是资助方。Terence Tao 指出,前两项直接有利于 AI 公司,第三项则预设了 AI 使用的必然性,他更希望由欧盟出资来制定集体标准。
Simons 基金会宣布与 Anthropic、OpenAI 合作,三方共同投入 1500 万美元资金与资源,由基金会管理和发放,用于支持帮助数学研究者评估近期 AI 辅助成果、学习使用新工具、交流观点并形成 AI 使用集体标准的工作坊与项目。
Terence Tao 博客发布 Deanna Needell 与 Hayden Schaeffer 的客座文章,征集数学家参与近期 AI 生成预印本成果的经历,包括提供前期结果、与 AI 模型互动、发表论文等。
上海人工智能实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型S2(书生-S2),通过人机协同完成困扰数学界30余年的三维Ghys猜想证明,论文已发布在预印本平台arXiv,形式化代码在GitHub公开。
入选理由材料完整呈现了人机协同证明数学猜想的流程与形式化验证环节,研究者可据此判断大模型在自身领域承担长程推导的可行边界。
作者提出 Euler,一个以共享结构化研究状态为核心的多智能体数学发现系统,记录精确命题与假设、命题间依赖、备选证明路线、失败尝试及每条结论的证据,供研究者和智能体共同使用。
美国数学学会(AMS)发布了一份基于其近期组织的数学科学研究生教育研讨会的报告。该报告于10月2日发布,由 Terence Tao 在其博客中提及。
一批 722 篇 AI 生成的论文被公开,令数学家开始争论这一领域是被摧毁还是被激活。目前尚不清楚 OpenAI 究竟以何种方式改变了数学,具体细节无人知晓。
Terence Tao 在其博客汇总了近期关于数学与 AI 的博客文章和评论文章,并邀请读者在评论区补充更多链接。收录的包括 Kevin Buzzard、Alexander Gamburd、Harald Helfgott、Gil Kalai、Asaf Karaglia、Matilde Marcolli 和 Fenner Stanley Tanswell 的文章。
数学家 Kate Stange 与 Edmund Harriss 在 Terence Tao 博客发文,讨论插画能否成为严谨的数学研究方式,相关文章已被 Notices 接收。
OpenAI 于 10 月 6 日在 GitHub 仓库发布 722 篇预印本,称其内部 AI 模型在几何、计算机科学、代数等 372 个数学问题上取得进展;10 月 7 日宣布因一处符号错误撤下 3 篇稿件,该错误使其中一篇的论证及两篇依赖论文的构造失效,另有 14 篇稿件做了证明修补、陈述更正等修改。
我一直相信,推进数学就是赋能数学家。 从我们在 @GoogleDeepMind 的最初日子起,我们的重点就是与数学界深度合作,并肩开创全新工具,拓展可能性的边界。
预印本论文提出 Kernel Autoresearch(Kernaut),让编码智能体以程序形式编写核函数组件,由可信解释器按保正半定的构造契约组装,只有通过 Tier 2 校验的程序才进入质量-多样性存档。
2026 年 9 月 11 日,MIT 教授 Dor Minzer 收到朋友短信,询问他是否即将解决理论计算机科学中最著名的开放问题之一。Minzer 是“唯一游戏”猜想领域的顶尖专家,起初以为这是玩笑,随后更多消息接连传来。