AI 能做数学，我们为什么还做数学？｜采薇｜坐标跃迁

AI 怎样改变数学研究？当形式化证明可以交给机器检验，什么样的工作仍然值得人去做？ 《坐标跃迁》首期访谈，Rand 与采薇（化名）——一位从事 AI for Math 与形式化数学研究的数学学生——从类型论、Lean 和形式化证明聊起，讨论“低垂的果实”、算力与研究资源，以及为什么一个正确的证明，仍然需要被人理解、整理和复用。 谈话也逐渐回到更个人的问题：为什么选择数学？当熟悉的能力和研究路径开始变化，我们如何判断自己的价值，又如何继续前进？ 在访谈最后，采薇谈到“保留迷惘的权利”：不必先想清楚每一件事，才能开始行动。 主持：Rand 嘉宾：采薇（化名） 时长：46 分 13 秒 中文访谈，中英双语字幕。 English description What is AI changing about mathematical research? When machines can check formal proofs, what work remains worth doing for people? In the first Frame Shift interview, Rand speaks with Caiwei—a pseudonym—a mathematics student working on AI for Math and formalized mathematics. Starting with type theory, Lean, and formal proofs, they discuss “low-hanging fruit,” access to computing and research resources, and why a correct proof still needs to be understood, organized, and reused. The conversation also becomes personal: Why choose mathematics? As familiar skills and research paths change, how do we understand our own contribution—and keep moving forward? At the end, Caiwei reflects on “reserve the right to reverie”: allowing room for uncertainty while continuing to think and act. Host: Rand Guest: Caiwei (pseudonym) Duration: 46:13 A Chinese-language conversation with Chinese and English subtitles. 章节 / Chapters 00:00 开场介绍 / Introduction 00:52 AI 与形式化数学 / AI and formalized mathematics 04:09 AI for Math 的进展 / Developments in AI for Math 17:14 低垂的果实与算力资源 / Low-hanging fruit and computing resources 23:24 数学研究与实验 / Mathematical research and experimentation 26:49 形式化与人机证明 / Formalization and human–AI proofs 32:01 为什么继续做数学 / Why continue doing mathematics? 40:59 数学的价值与迷惘 / The value of mathematics and uncertainty 封面为 AI 生成图像。 / Thumbnail generated with AI.