如果数学不止证明，我们该如何庆祝其余部分
If math is more than proof, we need to better celebrate the rest of it
我是 Grant Sanderson，来自 3blue1brown。当前数学界面临一个核心问题：当 AI 能自动生成证明时，数学家的价值何在？我认为，证明只是手段，真正的目标是增进人类理解。如果证明可以脱离理解而存在，我们就需要重新定义学术奖励机制。我提议赋予“动机解释”（motivated explanation）与证明同等的学术地位。这并非指科普，而是指那些能回答“你是如何想到这个的”的深度工作。从 Timothy Gowers 编辑《Princeton Companion to Mathematics》到 Bill Thurston 的几何中心项目，再到 Liam Price 利用 GPT-5.4 Pro 解决 Erdős Problem 1196，这些案例都表明，将“从 0 到 1”的证明转化为“从 1 到 N
HN 评论区
248- ForgotMyUUID
我不禁想起 1900 年巴黎国际数学家大会上庞加莱与希尔伯特那场著名的辩论。当时大家决定追随希尔伯特，证明的地位开始凌驾于直觉之上。我认为现代学校数学和应用型大学数学在某种程度上已经丢失了这种直觉。我试着告诉我的学生，数学首先是一种极其精确的交流语言。有时候我会觉得很有趣，让那些不喜欢数学的人完全不用数学，看看描述周围事物会变得多么困难。其次我告诉他们，公式是机制最纯粹的形式。在这种形式下，它们更容易被理解和在脑海中操作。修完力学课后，我总爱想象，对于任何公式，你都能可视化一个实现它的机制或过程。第三点，我想是验证自己陈述的能力，即证明。当然，数学家们可能会因为我的异端邪说而把我撕碎：抱歉，我不是数学家，而是工程师。你可能会因为使用错误的假设而犯错，但在某个节点，分析本身会向你展示你错了。有一本很棒的书，《How to Prove It》（作者 Daniel Velleman），为像我这样的初学者提供了证明入门。我真的很喜欢它。
- sweezyjeezy
数学界正在面对程序员几年前就开始应对的局面，只不过更加激烈。如今软件行业的护城河似乎是：AI 可以自动化任务，但（暂时）还无法替代整个工作。但对于很大一部分数学家来说，做这些任务本身就是 _那份_ 工作。那是他们想做的事，如果他们完成了一套足够困难的任务，就能获得终身教职。现在这个模式正在失效，他们迫切需要转变人类的角色，以挽救其专业免受资金削减的影响。
我记得当“写代码从来不是重点”在这里成为一句口号时。这话有几分道理，但去掉编码确实带走了工作中许多质感和工艺的乐趣。许多人在作为团队技术主管带领 AI 代理团队以获取收入时，都感受到了这种失落。我不乐观数学界的转型会成功，但我确信，即使他们成功了，大多数人也会因结果而感到沮丧。
我们都在凝视着同样的存在主义恐惧，只是看到它展开得更慢罢了。有人告诉我们，乌托邦就是被淘汰，这是一个令人震惊的概念。
- contubernio
我是一名职业数学家。今天我证明了一个对我来说非常坚实的定理。这是我思考了几年的东西。经过几周认真使用 AI，我找到了一个证明，目前正在撰写，但看起来是正确的。工作流程的变化是巨大的，但如果你清楚要做什么以及怎么做，你能做的事情也是巨大的。
- youoy
这里的争议部分在于，现在某些菲尔兹奖得主所具备的技能优势已经大大缩小。菲尔兹奖设有年龄限制这一事实，意味着它更看重脑力而非理解力。而这曾是该社区的指导灯塔。所以，当他们被 AI 冒犯时，我觉得这既“有趣”又自然。
这就是数学的主要“危机”。
在我看来，从来没有任何时候比现在更适合做数学家，也从来没有任何时候比现在更适合做软件构建者。
但从来没有任何时候比现在更糟糕，当你需要单独证明你作为数学家或软件工程师的经济价值时。因为“理解”不是你能在一个下午证明的东西，而是你用一生去证明的东西。
- bonoboTP
去年夏天，Grog 还因勇敢地用长矛刺穿动物并把肉带回家而备受赞誉和钦佩。但现在 Goong 发明了这种新奇的弓箭装置，任何懦弱的傻瓜现在都可以从远处射杀动物了。Grog 贬值了。Grog 很伤心。
- kurthr
从我对 Gower 最近关于此主题帖子的个人感悟来看，这正朝着一个必要的方向发展。
数学正遭受古德哈特定律（Goodhart's Law）的困扰：
“当一个指标成为目标，它就不再是一个好的指标。”
- bobajeff
让我们看看模型需要多久（如果会发生的话）才能生成带有动机的解释（可能通过 Manim 库或类似工具实现），同时附上它们的 Lean 证明。Grant Sanderson 说得对，这在某种程度上是主观的，但艺术也是如此，我对 AI 生成的艺术非常热衷。
- c7b
> 我们可以想象一下，为开放式阐述问题设立类似“千禧年大奖难题”的奖项会是什么样子
核心思想在我看来，我们应该将专业评估的标准从生成证明转向生成解释。这样的提议出自 3B1B 那位博主之手是有道理的，而且我实际上同意这一观点，无论是否有 AI。但让我困惑的是，这如何能成为对抗 AI 将人类自动踢出数学界的防御机制。AI 在生成自然语言解释方面可能并不比生成严谨证明差多少。值得注意的是，就连 Terrence Tao 也转向 AI 来理解 AI 生成的结果 [0]。这篇文章似乎完全没有解决这个问题。