本期嘉宾：Leonardo de Moura，Lean创始人、AWS高级首席科学家、SAIR Foundation研究合作伙伴，此前在微软研究院开发Z3定理证明器。 【时间线】 02:30 Lean入门：把数学证明当成编程，Natural Number Game作为游戏化学习 08:00 AI的"幻觉"问题：强大但不可靠，数学证明需要100%正确 14:20 Lean的解决方案：验证AI输出，人类专注高抽象层次 20:00 AI在日常研究中的角色：回音板、文献导航、代码维护、行政助手 28:40 职业影响：重复性工作消亡，新职业诞生（以"域名销售"为例） 35:00 给年轻学习者：AI作为Lean和数学的入门向导 42:10 Lean的技术演进：从Z3的全自动到人机协作，再到AI辅助证明 50:00 未来方向：为AI优化Lean，处理人类无法消化的大量信息 56:30 彩蛋：π的记忆衰退史 【核心观点摘录】 "View Lean as a programming language. The same way you use Python to write programs, you can use Lean to write math." "AI is very powerful, but it hallucinates. We need to make sure we don't have to check if the proof AI found is correct or not." "It enables us to work at a much higher level of abstraction. We don't need to focus on the details, but you can ensure they are correct because Lean is checking them." "If your job is just resist [execute], it may be affected by AI. AI is a queue to it, super fast." "I believe you will have many more people creating professional contents. You have an idea but you are not a designer, you don't know how to create compelling animation—AI will help you." 【适合谁听】 * 对形式化数学证明感兴趣的程序员 * 担心AI"幻觉"的研究者 * 思考AI对软件开发职业影响的从业者 * 想入门Lean或定理证明的学生

本期嘉宾Damek Davis，宾夕法尼亚大学统计与数据科学系副教授，与菲尔兹奖得主陶哲轩共同发起"数学蒸馏挑战赛"。 内容索引 00:00 国际数学日背景与π的记忆 03:20 优化常数列表：与陶哲轩、Doron Zeilberger合作的100个数学常数项目 08:15 数学蒸馏挑战赛的起源：从拓扑学反例到等式理论 15:40 核心机制：将推理过程蒸馏为"备忘单"式提示词 24:30 等式理论作为测试案例：封闭世界与完备知识的优势 33:10 问题诊断：数学家使用AI效果不佳的结构性原因 42:00 提示工程的方法论本质：类比指导研究生 51:20 未来阶段：反例生成与Lean形式化证明 58:00 提示优化器（Prompt Optimizer）的技术脉络 核心论点 Davis提出，当前数学家与AI协作的低效，核心在于缺乏将专业思维转化为机器可理解指令的能力。数学蒸馏挑战赛通过竞争性机制，系统性地探索这一转化过程的形式化方法。 关键区分 * 封闭世界推理：等式理论的规则边界明确，便于客观评估 * 开放世界推理：未来拓展至更复杂的数学领域 * 分类任务：当前阶段仅判断蕴含关系 * 构造任务：未来阶段要求生成反例与证明 相关资源 * 优化常数列表：Davis个人网站 / 陶哲轩GitHub * 数学蒸馏挑战赛：官方入口 http://sair.foundation

核心内容：Sebastian Bubeck讨论了OpenAI的AGI目标、AI作为真正协作者的条件，以及"AI物理学"研究。 亮点： 1.明确OpenAI的终极目标是AGI（通用人工智能），而"AI for Science"是AGI的最佳应用场景 2.认为AI在数学领域已经成为真正的协作者 3.提出成为真正协作者的关键：提示工程（prompting）仍然重要，需要详细说明背景、目标和期望的反馈类型 4.介绍"AI物理学/AGI物理学"：从参数级、神经元级到token级等不同粒度理解AI，希望借此构建更好的模型 5.分享GPT-5寻找不等式证明的过程：需要构建"思考工具（harness）"让模型长时间思考，期间不断产生新想法、整合旧想法、自我批评 6.强调领域专业知识比以往任何时候都更重要，只有深入理解才能充分利用AI模型，避免过度依赖而不理解底层原理

核心内容： Jiantao Jiao讨论了世界模型、AI在模拟中的应用，以及通用模型与专用模型的共存。 亮点： 1.介绍世界模型（World Models）概念：利用AI增强传统模拟方法，构建高质量的模拟器环境，让AI能够快速预测环境状态变化 2.强调AI应该能够分配准确的不确定性估计，帮助识别数据稀缺区域和极端事件，指导下一步探索 3.提出未来将是通用模型与专用模型"干预与共存"的格局：通用模型提供基础推理能力，专用模型针对特定领域数据和应用 4.指出AI正在降低科学参与门槛，让训练时间较短的人也能参与发现过程，但这也需要更好的合作机制来确保质量

核心内容：Hoifung Poon分享了他在微软研究院15年领导AI研究和医学发现孵化的经验，讨论了技术落地的复杂性。 亮点： 1.提出"技术只是催化剂"，真正的挑战在于重新想象整个工作流程、商业模式和组织原则 2.以医学发现为例，强调需要"超越技术的村庄"——包括公众教育、社会契约重新思考、隐私合规和监管等 3.建议采取"雄心勃勃但从小处着手"的策略，建立"飞轮效应"：从最小可行成果开始，快速展示ROI，逐步积累资源解决更大问题 4.讨论了涌现能力（emerging capability）现象：通用模型在足够大的数据和参数规模下，会在特定任务上展现出意外性能

核心内容：Erran Li讨论了自我改进智能体、形式化验证系统以及AI在科学发现中的协作模式。 亮点： 1.研究重点是自我改进智能体在计算机使用、数学编码和最近扩展到的证书发现（Certik discovery）等领域的应用 2.强调通过可验证奖励（verifiable rewards）来确保推理模型与真实对齐，减少对人工反馈的依赖 3.认为Lean等数学验证程序代表了未来趋势，将逐步实现更多自动化验证 4.提出AI在科学中的最佳协作模式：目前科学家在循环中（scientist in the loop），未来将发展为实验室在循环中（lab in the loop）的闭环系统 5.指出人们常犯的错误是将模型当前能力与近期能力混为一谈，低估了AI的快速发展速度（3-6个月内的变化）

核心内容：Damek Davis教授讲述了他从纯数学转向优化理论和机器学习的经历，以及对现代AI系统挑战的看法。 亮点： 1.回顾了自己从交换代数几何转向计算机视觉，最终专注于优化理论的"曲折道路"，因为发现解决机器学习问题需要更好的优化算法 2.指出现代AI面临的最大挑战之一是上下文长度（context）问题，希望未来模型能处理更长的上下文（如100页风格指南） 3.提到"递归语言模型"等新兴技术，让AI能够编辑自己的上下文 4.正在策划一个数学优化常数集合作为AI基准测试，包含从《数学年鉴》等顶级期刊中的难题 5.强调不同领域对"真理"的标准不同：数学需要100%准确，物理学有理论派和实验派之分，医学则依赖随机对照试验 收起

核心内容：Andrea Bertozzi教授分享了她在应用数学领域30年的研究经验，特别是近10-15年将数学与机器学习、AI结合的工作。 亮点： 1.强调AI与科学之间的"交叉授粉"（cross-fertilization），认为组织应该搭建科学家与AI算法开发者之间的桥梁 2.举例说明数学在DNA折叠和单链DNA适配体设计中的应用，展示了基础数学与机器学习结合解决化学问题的潜力 3.提出"可解释性是一个移动的目标"，作为数学家，她将可解释性定义为能够在基础层面理解算法、证明相关理论并预测其行为 4.分享了将流体力学中的表面张力概念应用于高维图数据的研究，展示了跨领域思维的价值