数学2024ams.org
机器辅助证明
Machine-Assisted Proof
入门 · 约 45 分钟读完前置知识：数学证明基础、Lean 定理证明器、大语言模型基础
导读
这篇 AMS Notices 文章讨论机器辅助证明在数学研究中的现状与前景，尤其涉及 LLM 辅助写 LaTeX、用 Lean 形式化证明等用法。评论所引的作者经验是：当前模型（如 GPT-4/Copilot）建议质量参差但确有帮助，更值得期待的是下一代模型与 Lean 的结合。
HN 关注点：顶尖数学家公开为 LLM 进入纯数学“正常化”背书，以及随之而来的关于数学之美、机械化、隐私与利益动机的争论。
HN 评论精选
这几条评论里：支持 1 质疑 2
支持认为这是顶尖数学家对 LLM 辅助纯数学的正式背书和正常化，对数学界意义重大。
我会称这篇论文是件“大事”：它来自纯数学领域一位领军人物，意味着 LLM 在纯数学中的使用被正常化、得到相当公允的总结，并显示出有未来。在 HN 上，我们过去几年已经大量讨论和思考 LLM，所以这篇论文对数学好奇的 HN 读者可能没太多惊人内容。但外面有一大批研究数学家可能对现代 AI 了解不多；Tao 是在说上一代模型（GPT-4）已有一点用处，并预计下一代模型与 Lean 结合会有很大用处。如果你读过他的博客，这不意外，但我认为在 AMS 发表一篇完整论文是相当重要的时刻。
vessenes查看英文原文
I'd call this paper a "big deal" in that it is a normalization of, very fair summary of, and indication that there is a future for, LLMs in pure mathematics from one of its leading practitioners. On HN here, we've spent the last few years talking and thinking a lot about LLMs, so the paper might not include much that would be surprising to math-curious HN'ers. However, there is a large cohort of research mathematicians out there that likely doesn't know much about modern AI; Terence is saying there's a little utility in last-gen models (GPT-4), and he expects a lot of utility out of combining next-gen models with Lean. Again, not surprising if you read his blog, but I think publishing a full paper in AMS is a pretty important moment.
质疑质疑 Tao 对 ChatGPT/Copilot 的背书，指出隐私、版权和利益动机等问题未被讨论。
“我发现它在写数学 LaTeX 以及用 Lean 形式化方面出奇地好用；事实上，它在我写这篇文章时建议了好几个句子，其中许多我保留或稍作编辑后放进了最终版本。虽然建议质量参差不齐，但有时会展现出对文本意图的、不可思议的模拟理解。” Tao 是少数一直在盛赞 ChatGPT 和现在 Copilot 的数学家之一。他似乎不介意自己的思考过程被一家市值数十亿美元公司的服务器记录。他从不提版权或社会问题，也从不提“写 LaTeX 更容易”之外的结果。他是否有推广 OpenAI 的动机？
kartwna查看英文原文
"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the text." Tao is one of the few mathematicians who is constantly singing the praises of specifically ChatGPT and now CoPilot. He does not appear to have any issues that his thought processes are logged by servers owned by a multi-billion dollar company. He never mentions copyright or social issues. He never mentions results other than "writing LaTeX is easier". Does he have any incentive for promoting OpenAI?
质疑批评 AI 的创造性辅助会让数学机械化、失去美感，并以国际象棋作类比。
我认为他把这次与以往的机器辅助相提并论有误导性。以往机器从不具创造性，而现在 AI 能提出创造性的路线。短期看很令人兴奋，但我也认为这削弱了数学之美，因为它把数学机械化成了生产真理的流水线，削弱了人类在追寻真理中的体验。国际象棋也发生过类似的事：越来越多人提倡 Fischer random，因为用电脑准备开局、研究棋局很无聊。当然电脑并非深度开局准备的起点，但它把它推到了新层次。关键是机械化除了纯实用之外很无聊。我的观点是，数学作为美的事物正在被机械化，会让潜在感兴趣的人对数学同样冷漠。现在还是蛮荒西部、有东西可摸索所以兴奋，但未来呢？我认为在数学中使用先进 AI 是个错误。作为人类事业的真理追寻令人鼓舞；工业化生产真理则很无聊。
vouaobrasil查看英文原文
I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same thing has happened in chess, with more people advocating for Fischer random because of the boring aspect of preparing openings with a computer, and studying games with a computer. Of course, the computer didn't initiate the process of in-depth opening preparation but it launched it to the next level. The point is that mechanization is boring except for pure utility. My point is that math as a thing of beauty is becoming mechanized and it will lead to the same level of apathy in math amongst the potentially interested. Of course, now it's exciting because it's still the wild west and there are things to figure out, but what of the future? Using advanced AI in math is a mistake in my opinion. The search for truth as a human endeavor is inspiring. The production of truth in an industrialized fashion is boring.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
- 视频与演讲
历次讨论
- 2024Hacker News 讨论帖199 分 · 96 评
同领域还值得读
一种新的相关系数
A New Coefficient of Correlation
提出了一种新的相关性系数（由 Sourav Chatterjee 提出），能够检测变量之间任意形式（不限于线性）的相关关系，且计算简单高效，主要基于排序和距离计算。
数学2021 · 682 分 · 158 评 · 引用 1进阶 · 约 60 分钟编辑精选数学的两种文化
The Two Cultures of Mathematics (2000)
这是数学家 Timothy Gowers 于 2000 年发表的一篇随笔，他把数学研究大致分成两种文化：一类是“解题者”，热衷于攻克具体难题、发展技巧（如组合数学）；另一类是“理…
数学2009 · 307 分 · 102 评入门 · 约 35 分钟编辑精选重新定义统计显著性
Redefine statistical significance
提议将统计显著性阈值从常用的 p<0.05 收紧到 p<0.005，以降低假阳性率、缓解可重复性危机。
数学2017 · 303 分 · 114 评入门 · 约 45 分钟编辑精选统计建模：两种文化（2001）
Statistical Modeling: The Two Cultures (2001)
讨论统计学中两种建模文化：一种假设数据由某种随机模型生成，侧重推断与系数解释；另一种把数据生成机制视为未知，侧重预测精度，主张使用算法建模。
数学2015 · 254 分 · 36 评进阶 · 约 60 分钟编辑精选通信的数学理论 (1948)
A Mathematical Theory of Communication (1948)
这是香农 1948 年的经典论文《通信的数学理论》，奠定了信息论的基础。
数学2016 · 169 分 · 53 评入门 · 约 90 分钟编辑精选