随着AI数学管道变得越来越普遍，我们必须越来越多地面对一个重要问题： 我们为什么要关心解决难题？几乎总是，答案*不是*因为我们特别想要解决这个难题。 (1/12)

关于Navier-Stokes方程是否存在全局光滑解的问题在数学上是有趣的，这并不是因为答案本身非常重要，而是因为我们有理由相信，*发现*答案的过程很可能是... (2/12)

...以深入分析、偏微分方程、流体动力学等领域提供新的深刻见解，并利用新技术。解决费马大定理间接给我们带来了朗兰兹纲领。解决庞加莱猜想给我们带来了里奇流。人们希望解决纳维-斯托克斯方程能给我们带来同样重要的成果。(3/12)

确实，我们将这些问题视为“有趣的难题”，正是因为我们直觉上认为它们代表了我们当前理解和方法中的一个“空白”。这就是为什么那些声称用“技巧”或基础方法解决（例如）黎曼假设的怪人... (4/12)

...有些人似乎没有抓住要点：如果这些重大问题中的一个最终被证明可以仅仅通过现有的数学见解和技术来解决，那将是一个巨大的失望：我们曾认为涌流而出的泉水，实际上是干涸的。(5/12)

这与AI有什么关系？好吧，如果人们接受这样一个前提：困难的问题之所以有趣，主要是因为它们带来的新见解和理解，那么在AI发展的背景下，就会提出一个问题：谁对“理解”部分负责？ (6/12)

以穷举法进行证明（如四色定理），长期以来被认为有些争议，因为它们提供了证明的“认识确定性”部分，但不一定提供任何“洞察”部分（通常是我们关心的部分）(7/12)

因此，穷举法的证明当然不是“错误”的，但在某种意义上它们是“作弊”的，或者说是“自我挫败”的：它们关闭了一个潜在的有益问题，同时忽略了数学中那些使其有趣和有价值的方面。 (8/12)

我认为，在生成这些证明的人缺乏任何理解或洞察力的情况下，AI生成的证明应该被视为类似的。如果你自动生成了一个大定理的Lean证明，那很好！但你为什么要这样做？ (9/12)

如果你不理解证明中包含的新见解/方法，那么你所做的只是将智力负担从自己转移到任何愿意阅读和理解它的人身上（并且，希望能够将其中的见解传达给他人）。 (10/12)

数学最终是人类文化的产物（可能是我们最深刻、最丰富和最古老的）。解决困难问题本来只是扩展这一产物的*代理*。AI 使得生成新的数学理解路径变得令人兴奋地简单.. (11/12)

...在那个文物中，但它也使得实现代理（即解决困难问题）比以往任何时候都更容易，同时却忽视了我们最初关心的整个原因（即加深我们的理解）。 请不要这样做。 (12/12)