Lean 联合作者 Avigad 发文：数学家应主动拥抱 AI 而非抵御
keviv9 · x · 2026-10-10
CMU 教授、Lean 定理证明器 2015 年原始论文合著者 Jeremy Avigad 在 Math, Inc. 宣布完成球堆积形式化之后发表新论文，回应「数学家如何面对快速进步的 AI for Math 浪潮」。
- 文中披露了 Math, Inc. 公布成果背后的故事，以及参与形式化项目的人类研究者最初收到消息时的反应。
- Avigad 的核心结论：数学家的优势在于解决问题和构建理论，与其抵抗 AI 在数学中的应用，不如主动掌控它——不能只跟进展、给 AI 研究者设计 benchmark，而要在技术的部署和使用中扮演积极角色。
「漫话AGI」频道最新
- 参观巴尔的摩工业博物馆有感:技术史讲解只剩失业与不平等叙事 — Afinetheorem · 2026-10-10
- AI 没有杀死创意工作，而是改变客户付费方式 — kevinsurace · 2026-10-10
- AI 给你的菜谱不是它创作的：原作者被系统性抹去 — gerardsans · 2026-10-10
- KKT 点对应 CDT+GT 均衡：不完美记忆博弈与策略梯度优化的理论桥梁 — jessi_cata · 2026-10-10
- 意识研究圈玩梗：对着「心灵空间」分类图扔飞镖 — eigenhector · 2026-10-10
- 把《三体》当 AGI 预言读:刘慈欣是否早写过超对齐? — abhiadesai · 2026-10-10