张小珺Jùn｜商业访谈录 - 第137期
对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的
概要
这一期，主持人张小珺与数学与AI领域的前沿人物洪乐潼展开了长达四小时的深度对话。节目围绕AI for Math（人工智能与数学的结合）、利用Lean软件形式化数学证明、解读“数学天书”中的难题与证明、数学直觉的来源，以及数学本质是“被发现”还是“被创造”这些核心议题。洪乐潼以其独特的经历和视角，将严肃的数学理论与个人思考交织，为听众带来富有思辨与启发性的讨论。
主要讨论点与精彩摘要
1. AI for Math：人工智能如何改变数学 (10:22 - 44:36)
- AI与数学结合的现状与前景
洪乐潼从AI辅助数学研究的现有进展谈起，包括AlphaFold、OpenAI的数学推理模型等。人工智能在攻克传统被认为“只靠人类大脑才能完成”的问题上，正发挥越来越关键的作用。
洪乐潼（15:10）：“AlphaFold 其实就是AI for Science的典型案例。虽然目标不是直接证明定理，但它让我们看到了AI能补全人类未知的那部分。”
- AI在数学证明中的当前困境
洪乐潼坦言，AI目前还无法从根本上理解抽象的数学意义，更类似于“形式游戏”。
洪乐潼（22:45）：“其实现在所谓的AI for Math，更多集中在‘形式化’和‘搜索空间’。它还谈不上理解数学。”
2. 把数学变成Lean：形式化证明与实践 (45:00 - 1:32:18)
- Lean软件的革命性意义
洪乐潼详细介绍了Lean作为数学定理验证工具的优势，以及“为数学写代码”的全新体验。
洪乐潼（56:28）：“用Lean证明一个定理，有时候比手写证明还难。但你能确定，这个证明是真的对，不会丢掉任何环节。”
- Lean社区的成长与变革
Lean的开源社区如何推动大规模合作，改变传统“孤独的数学家模式”。
洪乐潼（1:10:33）：“Lean 社区其实很接近开源软件社区，大家会协作、会像工程师那样review贡献，这和以前数学是发表论文完全不一样。”
3. 解读数学天书：难题、证明与数学的美 (1:35:02 - 2:55:40)
- 攻克“天书”级别的问题
洪乐潼分享了“天书”级别难题的个人攻关经验，背后是对美的直觉和痛苦的挣扎。
洪乐潼（1:48:19）：“有一些定理，第一眼真的像天书一样，一点线索也没有。你只能靠直觉，一点一点摸。”
- 数学证明的直觉与理性
讨论“直觉”在数学发现中的作用，以及如何在数学和AI间实现直觉与理性的平衡。
洪乐潼（2:15:59）：“其实数学家直觉很强，有时你先猜到结论，但需要理性的证明过程。AI 目前还很难模拟这种直觉。”
4. 数学的本质：被创造还是被发现？(2:58:21 - 3:46:09)
- 关于“数学存在论”的思辨
洪乐潼和张小珺展开关于“数学是人类发明还是宇宙客观存在”的讨论。引用历史上的经典争论，并结合个人体验。
张小珺（3:02:13）：“你觉得数学是被造出来的，还是本来就在那儿只等人类发现？”
洪乐潼（3:03:44）：“我的直觉是，它既有主观的一面，也有某种客观性。就像圆周率，有人类之前它在不在？也许‘在’，但没被看见。”
- AI在数学本质问题上的作用
探讨AI是否会颠覆人类数学发现的方式，推动对“普遍真理”的更深追问。
5. 技术进步与新世界的可能 (3:46:20 - 4:13:20)
- 未来的数学家会是什么样？
洪乐潼描述了AI、工具和社区影响下，未来数学家创作和协作方式的巨大变革。
洪乐潼（3:50:58）：“如果AI能像辅助写作一样辅助数学家，大家是不是会解放出来，去想更难的问题？”
- 数学与人生的共振
节目最后洪乐潼谈到，数学不仅仅是工具，也是人生、世界观的一种折射。
精彩金句回顾
- “数学的乐趣，就是和未知不懈地赛跑。”
—— 洪乐潼（00:52:05）
- “Lean 就像一把尺子，把所有细节不厌其烦地量一遍，让你不得不严肃对待每句话。”
—— 洪乐潼（57:13）
- “也许数学最美好的地方，就是它做到了在很纯粹和很混乱之间切换。”
—— 张小珺（2:31:29）
重要片段时间线
- 10:22 — AI for Math现状与AlphaFold
- 22:45 — 现阶段AI对数学理解的局限
- 45:00 — Lean形式化工具的介绍
- 1:10:33 — Lean开源社区与数学协作
- 1:48:19 — 攻克天书难题的体验
- 2:15:59 — 直觉与AI的对比
- 3:02:13 — “数学是创造还是发现？”
- 3:46:20 — 技术对未来数学家的影响
总结
整个访谈以温和而深刻的风格，贯穿数学与AI前沿、工具革命、证明艺术与哲学思辨。对于关心人工智能、数学未来，以及科技与人文交融的人来说，这是一场知识密度极高、回味悠长的思想盛宴。
