1
0本期嘉宾：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或定理证明的学生
