Tao Lab

← 返回 Dashboard

访谈/播客

Leonardo de Moura 的圆周率日寄语：形式化证明、Lean 与数学的未来

Happy π Day from Leonardo de Moura: Formal Proofs, Lean, and the Future of Math
访谈/播客🎤 嘉宾：Leonardo de Moura（莱昂纳多·德·莫拉，Lean 与 Z3 的创造者）；主持/访谈：Maddie（一位学生主持人）；开场：Chuck（SAIR 联合创始人）⏱ 13:55👁 NA
▶ 在 YouTube 观看
在圆周率日，Lean 之父 Leonardo de Moura 接受学生 Maddie 访谈，深入浅出地讲解形式化证明工具 Lean、AI 如何与之结合，以及 AI 将如何改变数学发现与未来职业。

核心要点

分章详解

开场与嘉宾介绍

  • SAIR（科学与 AI 研究基金会）联合创始人 Chuck 开场，介绍这是一个圆周率日（Pi Day）项目，并把时间交给主持人 Maddie。
  • Maddie 介绍嘉宾 Leonardo de Moura：创造了 Lean 的计算机科学家，Lean 是帮助数学家和程序员检查证明与程序的工具。
  • 整段为轻松的师生式问答风格，de Moura 多次以面向中学生的语言作答。

用最朴素的方式解释 Lean

  • de Moura 把 Lean 类比为编程语言：就像用 Python 写程序一样，可以用 Lean 来「写数学」。
  • 他提到面向年轻学生的入门方式——「自然数游戏（natural number game）」，是 Lean 的一个更受约束的版本，可以像玩游戏一样学数学。

AI、Lean 与数学发现的改变

  • 他认为 AI 会「极大地」改变数学发现的方式：AI 强大但会产生幻觉，Lean 则负责确保证明的正确性。
  • Lean 让人能在更高的抽象层级工作，不必纠缠细节，因为正确性由 Lean 来检查。
  • 谈到自己日常对 AI 的依赖：当作讨论新想法的「回音板」、推荐该读的论文、快速学习新领域、整理日程、写提案、写 Lean 代码，以及帮助维护 Lean 庞大库之间的一致性（同步）这种「耗费大量精力的苦活」。

AI 对就业的影响：被取代与被创造

  • 他同意数学领域会被 AI 加速而非简单取代，因为总有人类意想不到的新东西不断涌现。
  • 受影响的是「纯执行性」的机械重复工作——大团队里只有少数人驱动创新，其余执行者的角色可能被 AI 取代。
  • 他以农业和软件开发类比：未来团队规模更小却产出更多；并讲述朋友早年「在互联网上卖域名」的故事，说明今天难以想象的新职业会出现。
  • 他预测未来会有更多人借助 AI 创作专业内容（如动画、设计），「有想法」比「会执行」更重要，教育材料的质量和产出速度将大幅提升。

给好奇学生的建议

  • 技术安装等障碍可以交给 AI：想试 Lean 就直接和 AI 对话，它会一步步教你安装、上手。
  • 把数学问题或项目告诉 AI，它能给出攻克角度的反馈、提供入门指引、按你当前水平给出练习题。
  • 他强调如今深入数学的门槛与十年前已截然不同，AI 可充当个性化「向导」。

个人经历与 Lean 的诞生

  • 他 12 岁拥有第一台计算机后就「上钩」了，从此再无疑虑地知道自己要做什么。
  • 他出身于「自动推理（automated reasoning）」领域，此前做了全自动求解器 Z3（取名自一款汽车），用于约束求解，例如把软件找 bug、安全漏洞问题表述为可判定的数学问题来自动求解。
  • 有用户想把 Z3 用于软件验证，但验证问题是不可判定的、依赖启发式，因而不稳定；一位用户说「我已经知道证明了，只想把证明告诉系统」——这正是 Lean 的起点：把全自动世界与可交互世界结合。
  • Lean 诞生于 AI 之前，但为人类设计的交互机制后来恰好让 AI 受益：AI 如今用同样的机制来引导和控制证明器。

为 AI 优化 Lean 的未来

  • Lean 过去为人类优化，未来要为 AI 做得更好：让 AI 能快速迭代，每次调用近乎瞬时，反馈循环高效。
  • 面向人类时需过滤信息量（人类注意力有限，无法消化数千行反馈），而 AI 能处理海量信息，提供更多信息有助其做更好决策。
  • 他对未来乐观：如果 Claude 和 Gemini 现在就能用 Lean 做这么多，未来还能做得更多。

圆周率日彩蛋收尾

  • 应景提问能背几位圆周率：de Moura 笑称年轻时能背一串，现在只记得很少；主持人说自己只记得三位，两人「彼此彼此」。
  • 以「圆周率日快乐，继续探索数学之美」收尾。

关键引述

“把 Lean 想象成一门编程语言——就像你用 Python 写程序一样，你可以用 Lean 来写数学。（imagine Lean as a programming language the same way you use Python to write programs you can use Lean to write math）”— Leonardo de Moura
“AI 非常强大，但它会幻觉。Lean 确保你不必去检查 AI 找到的证明对不对。（AI is very powerful, but it hallucinates. Lean makes sure that you don't have to check if the proof AI found is correct or not.）”— Leonardo de Moura
“有一位用户告诉我：我已经知道证明了，我只是想把这个证明告诉系统——Lean 就是这样开始的。（one of the users told me 'I know the proof, I just want to tell this system the proof'. That's how Lean started.）”— Leonardo de Moura
“如果你的工作只是执行，它就可能被 AI 影响，因为 AI 执行得超快、又听从你的指令。（If your job is just to execute, it may be affected by AI... AI executes it super fast and follows your orders.）”— Leonardo de Moura
“如果你有一个想法，就跟 AI 聊——它会帮你把想法落地、帮你执行。（If you have an idea, talk to the AI to help you to execute on the idea.）”— Leonardo de Moura

术语 / 人物

Lean — 由 de Moura 创造的证明助手兼函数式编程语言，基于带归纳类型的构造演算，用于让计算机检查数学证明与程序的正确性，现广泛用于数学形式化与 AI 辅助定理证明。
Z3 — de Moura 早期创造的全自动 SMT（可满足性模理论）求解器，用于约束求解，可把软件 bug 查找、安全漏洞等可判定问题表述为数学问题自动求解。
形式化证明（Formal Proof） — 用严格的形式语言书写、可由计算机机械化验证的数学证明，确保每一步逻辑都正确无误。
幻觉（Hallucination） — 指 AI 生成看似合理但实际错误的内容；在数学场景下，Lean 可通过检查证明来兜底，防止错误结论被采信。
自然数游戏（Natural Number Game） — Lean 的一个更受约束的入门版本，让学生像玩游戏一样学习用形式化方式证明关于自然数的命题。
可判定 / 不可判定（Decidable / Undecidable） — 可判定问题能用算法判断真假（如 Z3 处理的片段）；不可判定问题（如一般软件验证、抽象数学）只能依赖启发式，因而不稳定。
Leonardo de Moura（莱昂纳多·德·莫拉） — 巴西计算机科学家，Lean 与 Z3 的主要架构师，现任 AWS 自动推理组高级首席科学家、Lean FRO 首席架构师与联合创始人。

背景补充

Leonardo de Moura 是巴西计算机科学家，自动推理与形式化验证领域的标志性人物，是 Z3 SMT 求解器和 Lean 证明助手的主要创造者（两者均始于微软研究院时期）。他现任 AWS 自动推理组高级首席应用科学家，并与 Sebastian Ullrich 共同创立、担任 Lean FRO（2023 年 7 月成立的非营利组织）的首席架构师。他屡获大奖，包括 Herbrand 奖、CAV 奖、Skolem 奖，以及两次 ACM SIGPLAN 编程语言软件奖（分别因 Z3 和 Lean）。本视频是 SAIR 在圆周率日推出的轻松访谈项目。

适合谁看

适合对 AI 辅助数学、形式化证明（Lean）感兴趣的学生、教育者与科技爱好者，尤其是想了解 Lean 是什么、AI 如何改变数学发现与未来职业的入门读者。