开源动态8

Axiom开源4310万行Lean数学证明

机器之心2026-10-28

AI 摘要

AI 数学公司 Axiom 组织数十个 AI Agent，耗时 24 天将 1.5 万页的有限单群分类定理转化为可验证代码，生成约 4310 万行 Lean 代码并全部开源。

纠错发现：揪出 1986 年论文等 34 处文献逻辑偏差

协作机制：自研系统协调多 Agent 分解任务并并行验证

额外产出：构造并形式化了一项全新的群论定理

关注公众号

扫码关注
第一时间收到每日精选

公众号专辑

陶哲轩邓煜呼吁数学「慢科研」

针对商业AI批量发布数学证明引发的争议，菲尔兹奖得主陶哲轩、邓煜在最新访谈中回应核心争议，提出AI解出问题不代表人类理解证明，呼吁保留数学「慢科研」的价值，讨论人机分工并推动开放数学工具开发。

本文报道菲尔兹奖得主陶哲轩发表《数学2.0》演讲，梳理近期AI接连攻克重大数学难题的进展，提出AI将数学带入证明过剩的新时代，警示人类不能丢失对数学的理解，呼吁人机合作增强认知。

本文报道谷歌DeepMind推出AI数学证明框架AlphaProof Nexus，破解多道悬而未决的数学难题含两道56年埃尔德什开放问题，成果经同行评审登上《Science》，对比OpenAI此前发布方式的争议，介绍其工作流程。

本文报道九章云极言表实验室在陶哲轩发起的数学蒸馏挑战赛第二阶段拿下全部赛道满分，解决28个未解决开放数学问题，介绍了其可验证AI+强化学习的AI4S布局。