8月,OpenAI宣布,其尚未发布的模型Astra在数学与计算机科学领域取得十项进展,涵盖几何、密码学与编码理论,并发布关于“对数学界的责任”的声明,承认归因、AI辅助结果正确性的问责及数学发现性质变化等关切。ChatGPT、Claude等大语言模型正冲击数学界:院系面临研究与教学中的伦理问题,期刊编辑委员会收到大量AI撰写论文并需决定如何评估与披露生成式AI的使用,arXiv数学投稿近期激增,资助机构开始制定AI使用政策。对于机器能否发现证明、构造例子或提出问题,人类数学创造力是否仍有独特价值,数学重在产出定理还是增进理解,以及贡献如何归属,数学界仍缺乏共识,部分数学家对学科未来感到焦虑。源文本末句中断。
相关动态
沿时间看主要节点
OpenAI发布了一批由其内部前沿模型生成的722篇数学手稿,涵盖数学与理论计算机科学领域的数百个研究问题,整理为372组相关成果,包含证明、替代论证、推论与支撑材料,其中不少结果附有Lean形式化证明。OpenAI表示,在现有数学评测表现开始趋于平台期后,团队把内部模型用于开放研究问题,评测过程约向模型提出4000道题;平均每项结果所用算力约相当于ChatGPT Pro思考三小时。公司同时强调,发布并不意味着所有结果都已完全验证,仓库中成果处于不同检查阶段,部分尚未在Lean中形式化的手稿可能含有错误;更正与修订会被记录,旧版本仍会保留。
OpenAI 在 2026 年 10 月 6 日的研究文章中宣布,将一个尚未发布的内部前沿模型产出的数学成果公开:openai/math 仓库以 Apache-2.0 许可发布 722 篇手稿,归入 372 个家族,并附 Lean 形式化证明与模型推理摘要。README 称绝大多数结果由同一套流程产生,评估过程中模型被给出约 4,000 道问题,平均成果所用算力约相当于三小时 ChatGPT Pro 的思考。并非所有手稿都配有 Lean 形式化,README 提醒部分未形式化结果可能存在问题,OpenAI 表示会尽快修正并保留公开发布历史。
OpenAI在GitHub上公布其新模型产生的372项成果,称每一项都解决或大幅推进了数学或理论计算机科学中的重大公开问题,其中包括四维Kakeya猜想的解法、对部分重要计算机算法的改进,以及朝Riemann猜想的实际进展。许多结果已在Lean(可校验证明逻辑的编程语言)中通过验证。OpenAI发言人告诉《Scientific American》,这款尚未公开的模型几乎所有结果都是对单个AI智能体的一个提示词作答所得;这与此前Navier-Stokes问题的解法不同——后者由一万个智能体组成的群体协作完成,耗费数百万美元算力。麻省理工学院数学家Andrew Sutherland表示,在OpenAI发布模型、结果可被复现之前,应把
Hexagon 是面向数学与理论计算机科学的新论文仓库,由多人自 2026 年 8 月初起合作筹建。作者认为借助 LLM 证明的结果大量涌现,需要新的收集模式:成果可被引用、可长期可靠保存,作者与社区参与门槛低于 arXiv,并为这些工作提供区别于 GitHub 仓库或 X/Bluesky/Mathstodon/LinkedIn 帖文的归属地。为支持项目,团队在特拉华州成立 Hexagon Mathematics Foundation,并拟申请 501(c)(3) 免税资格,作者出任首任执行主任。他举例说,与 FRG 资助团队合作时点击按钮即得到特征零四重子 Hodge 数的导出不变性这一新结果,他不愿署名而只在博客披露,如今该结果以 hexagon:2609.00104 收录于 Hexagon。
机器嗅觉的发展受制于数据稀缺与描述标签缺乏标准化,多源数据整合面临跨来源标注不一致、同义词冗余、分布偏斜等标签层面冲突。为此,作者提出SEA分类框架,将统计共现分析、专家香料学知识与基于百科全书及嗅觉科学文献定义的AI辅助语义对齐相结合。在此基础上构建了统一标签的气味数据集OdorNet,收录超过20,000条记录、9,000种独特分子,来源于1960–2021年学术文献与开放数据库,并整理为层级化标签体系。技术验证显示,基线模型在OdorNet上的Macro F1为0.42,明显高于常用气味数据集上的得分,也高于同一模型在不使用SEA标签体系的OdorNet上的得分。
Caltech 数学家联盟发表联合声明,重新设计 Mathathon 活动,新主题定为 Old Problems, New Proofs。发起者认为解题只是数学的一个组成部分,数学理解与阐释同样有意义,却常被资助方和招聘委员会忽视。参与者须挑选一个解答反直觉的问题(如四色定理、ABC 猜想、Navier-Stokes 问题),在 40 小时内尽可能深入学习并向同伴汇报,随后用两个月发展替代理证或阐释,提交 explainer 与 GitHub 仓库,公开 LLM 对话记录、可视化代码等材料。声明强调 Mathathon 把 AI 视为数学家可用的众多工具之一。
Radical Numerics 联合创始人 Eric Nguyen 讨论基因组语言模型与生物安全。他参与了 Evo 和 Evo 2 的开发;另一支 Arc/斯坦福团队随后用这些模型生成并合成了功能性噬菌体基因组。访谈区分了三个序列尺度:人类基因平均约 60K,较长基因可达 2.3M,而整个人类基因组约为 3B。Nguyen 认为,提升生物能力的模型也能帮助防御跟上能力进展。这里的 2.3M 指较长基因,不能写成全基因组大小。
陶哲轩与私人捐赠者共同创立非营利机构 Foundation for Science and AI Research(SAIR),支持 AI 在数学及其他科学中的负责任使用,独立于主要 AI 公司。初期资源有限,活动以播客、短会活动和竞赛为主;近期获 XTX Markets 与 Susquehanna 支持,用于资助下一轮 SAIR 竞赛。SAIR 正与学界、业界多个关键伙伴推进共建开放权重科学模型,以及面向科学应用使用开源与闭源 LLM 的开源工具。因当前局势与对开放模型的高需求,计划提前宣布,部分关键规划仍在进行中;目前正征集可提供资金、算力、专业知识或社区建设的伙伴意向,并提出共建 Math 2.0。
scBaseCount 目前是规模最大的公共单细胞 RNA-seq 数据资源库,收录了来自 27 个物种、75 种组织的超过 5.02 亿个细胞。一个 AI 智能体自主发现、注释并对 SRA 中的全部 10× Genomics 数据集进行统一流程的重处理,形成一个协调一致、持续更新的资源,用于研究细胞生物学的多样性并训练 AI 模型。
公开研究版图为未来研究方向预留了位置,不表示每一项实现均已完成或发布。公告当时,三个命名模块仍是分别排期的独立工作;原文明确说明它们尚不是已完成集成的产品。此条记录的是公告本身,不是这些未来发布的结果。
这是 PhAI Labs 技术报告,不是同行评审期刊论文。官网把发布日期标为 9 月 15 日,链接 PDF 封面标为 9 月 12 日;关联的 arXiv 预印本为 2609.15973,于 9 月 14 日 17:56 UTC 提交。报告提出研究框架并列举系统实例,但本身不证明后续模块已发布、已集成,或作为组合产品完成验证。
制药企业联合体报告称,用企业私有蛋白结构训练蛋白折叠AI模型可明显提升性能:研究者基于AlphaFold 3的开源复现版本OpenFold3,用超过20,000个专有结构训练新模型,表现优于仅用公开数据或各公司孤立数据集训练的模型。该研究以博客文章发布,尚未经同行评审,模型未公开。哥伦比亚大学计算生物学家Mohammed AlQuraishi认为这为建立类似公开数据集提供了依据;英国政府资助最高£800万(1,080万美元)的OpenBind项目上月已发布数百个结构。蛋白数据库(PDB)收录超过200,000个实验结构,但其中与类药物分子互作的结构可能仅约10,000个。
Google DeepMind 宣布已用 AI 预测人类 DNA 中全部 90 亿种单字母替换的生物学后果,并将结果数据库 AlphaGenome Atlas 免费开放给全球学术研究者。该数据库预先列出每个单碱基替换可能如何影响基因开关机制,此前研究者只能逐个变异运行模型或在实验室中验证,过程极其缓慢。研究副总裁 Pushmeet Kohli 称,这是首次有人
PocketScope 是一种免训练框架:它用冻结的 ESM-C 600M 嵌入表示空腔内壁残基,并通过穷举式晚期交互 MaxSim 检索相关结合位点,无需池化或近似最近邻搜索。在 AlphaFold 人类蛋白质组中,该方法在 37,682 个蛋白质里识别出 153,805 个空腔,并在精选药理学配对中找回有记录的药物脱靶。在 ProSPECCTs 基准的十个集合中,PocketScope 按平均排名位列 23 种方法中的第 1。PocketScope 已开源,并作为免费 Web 服务器提供(https://www.bhargavaresearch.org/pocketscope)。
提出运行时动作干预(RAI):保持策略参数不变,在推理后调节动作节奏并过滤已配置的动作模式;仅当冷却条件满足且内容检测器未标记动作时才释放,否则发送 no-op。检测器覆盖包括工人单位骚扰在内的毒性行为。作者在 AlphaStar actor.py 的复现中实现 RAI,并开源材料。在 StarCraft II 人类参与者研究中,同一高能力、动作速率受限的对手在隐瞒能力声明时,1-5分量表上的合并公平感、信任感、毒性感均值分别为3.90、3.50、2.00;披露时为2.62、4.31、2.85。披露在各专业组均对应更低的公平感和更高的毒性感;信任在新手与专家中上升,在中等水平参与者中下降。即使配置控制不变,用户感知也会随能力披露明显不同;因此人机评估须将执行栈内的控制与能力披露分开,将公平、信任、毒性作为独立维度。
公共基准是衡量自动语音识别(ASR)模型能力的重要手段,但模型可能针对基准进行优化,导致在真实数据上泛化不佳。本文提出一种量化基准优化的方法,聚焦于音频不足以确定参考转录文本的情况。研究者设计了三种行为探针:参考分歧、掩码数字恢复和正字法切换,以探测模型在音频不明确时复现基准参考片段的能力。结果发现,得分最高的开源模型即使在音频矛盾、掩码或模糊时也会输出逐字参考转录。通过多种机制探针,表明模型依赖狭窄的声学线索,覆盖音频的真实表征,转而采用基准优化策略。这些行为可通过低秩线性引导或音频拼接进行因果操控。总体而言,高性能模型表现出基准条件性行为,可能虚增基准分数,而不反映通用转录能力的提升。
陶哲轩近日宣布,Palomar——一个由 Lean FRO 和 ICARM 孵化的 Lean 验证数学注册中心现已开放提交。该中心旨在作为 Lean 证明的预印本服务器,接受包含挑战文件、解决方案模块和 formalization.yaml 的 GitHub 仓库快照。提交后,系统将检查解决方案模块是否类型检查并通过挑战文件中的声明,以及非正式描述是否与正式声明匹配。陶哲轩担任科学顾问委员会成员。这一举措旨在应对 AI 生成的 Lean 证明日益增多但验证困难的问题。
这是一个开放工具与工作流原型,不代表自主定理证明已经解决。项目页把 MathCode 标为 2026 年 4 月项目,当前列出的最新版本 v0.2.0 发布于 5 月 26 日;这里列在 8 月 16 日,是因为 Hacker News 讨论让它重新进入公共视野。最值得关注的是围绕 Lean 形成紧密的“编写—编译—诊断”闭环;已核验的项目页面没有给出证明成功率、基准对比,仓库也未显示明确许可证。
Aurora 1.5 是微软 Aurora 地球系统基础模型的重要扩展,新增 22 个与能源、农业、交通和气候风险相关的天气变量,并提供逐小时时间分辨率与概率集合预报。模型已在 GitHub 开源,Hugging Face 提供模型检查点,由 Microsoft Weather 在微软研究院 AI for Science 原模型基础上开发;Aurora 最初于 2024 年推出、2025 年发表于 Nature。新版本将开放研究连接到 Microsoft Weather 服务,支持数据、基础设施、托管访问和业务化应用,并加入了用户最需要的能力之一(原文在此处中断)。
一项跨物种基础模型创建了共享的细胞表征,支持在不同生物数据集间进行零样本迁移。该模型有望为细胞生物学研究提供通用的计算基础,促进数据整合与知识发现。研究强调了模型在跨数据集泛化方面的潜力,但具体技术细节未在文中详述。
机器学习原子间势(MLIP)正在变革计算化学与材料科学,但开发者面临缺乏GPU加速的原子模拟工具的问题。现有工具多为CPU中心,在混合工作流中,模型由PyTorch在GPU上加速,而模拟工具为串行CPU,导致效率瓶颈。NVIDIA在Supercomputing 2024上发布了ALCHEMI(AI化学与材料创新实验室),提供领域专用工具包和NIM微服务,包含GPU加速的批量操作,如邻居列表等,旨在弥合PyTorch与原子模拟之间的鸿沟。
本客座文章由Boris Alexeev撰写,介绍围绕Erdős问题的近期进展,特别是利用人工智能对旧新数学进行形式化。背景:保罗·埃尔德什提出了大量猜想,Thomas Bloom于2023年5月建立erdosproblems.com跟踪进展。2025年8月添加论坛,2025年5月Google DeepMind启动形式化猜想项目。Bloom和陶哲轩提议将网站与OEIS链接。目前网站上有1100多个问题,约40%已解决,约240个问题在Lean中形式化,17个有形式化解,260个链接到OEIS。文章还提及人类无AI形式化的早期例子,如Bloom和Mehta形式化单位分数问题。