数学2015arxiv.org
后人类数学
Post-human mathematics
进阶 · 约 60 分钟读完前置知识：数学基础、形式化验证、机器定理证明
导读
这篇论文探讨“后人类数学”问题：当计算机能够自动发现和证明定理时，数学是否还存在独立于人类大脑的结构与意义。核心争议在于机器产生的数学若人类无法理解，是否还有价值，以及“有趣/重要”的数学问题如何被机器识别。
HN 关注点：自动化定理证明与 AI 创造力的边界：机器生成的数学若无人能懂还算不算数学，这触及 AI、创造力和数学本质的哲学讨论。
HN 评论精选
这几条评论里：质疑 1 补充 3
补充自动数学的核心难题是识别“有趣”，类似艺术创作问题；机器证明未必不能人类化
我认为全自动数学最大的困难之一是发现“有趣”的东西。计算机数学若要脱离人类思维，总得有人付电费。既然没人会为定理空间中的随机点买单，机器必须能弄清人类到底想要什么——这很像计算机自动讲故事甚至艺术创作的问题。另外，机器证明的“外星感”未必是必然的：也许某天心理学家或哲学家能弄清人类认知喜欢什么，届时可以写一个输出人类友好证明的编译器。这引出一个有趣的问题：所有有趣的证明都能用人类友好的步骤构建吗？也许这正是我们还没解决 P 与 NP 的原因。
whatshisface查看英文原文
I think one of the greatest difficulties in completely automated mathematics would be the discovery of mostly those things which are interesting. If computer mathematics is ever to diverge from human thinking, someone must pay to keep the lights on. Since nobody would pay for random points in theorem-space, it must have some way of figuring out what the human brains down at the breaker box actually want. This to me looks a lot like the problem of computer automated storytelling or even art. Also, I don't think the alien-ness of computer proofs is a given. Perhaps someday some psychologist or philosopher might work out exactly what our cognition likes to work with, upon which time you could write a proof compiler that outputted those things. That raises and interesting question. Can all interesting proofs be built with human-friendly steps? Maybe that's why we haven't worked out P and NP.
质疑数学的价值依赖人类，但机器给出不可读却可机器验证的证明将带来根本性冲击
对“数学是否存在独立于人脑的结构”我倾向于回答“否”。人类认为“重要”的问题往往相当随意，如果后人类数学家每秒吐出几千页只有计算机能懂的数学，没人在乎——计算机在林中倒树，不会发出声音。但不排除未来“有创造力”的计算机产出人类无法解读却关乎我们关心的定理的证明，那将震动数学界：如果计算机以无人能懂的方式证明了黎曼猜想，但输出一份人人可加载验证的 Coq 文档，人们会认为问题解决了吗？
marcelluspye查看英文原文
> Is there a structure to mathematics which is independent of the human brain? I would venture to say "no". I don't think humans will ever have no place in mathematics, because the problems we deem "important" are often relatively arbitrary. If a "post-human mathematician" starts spewing out thousands of pages of mathematics a second, all in a form only a computer can understand, no one will care. If a computer fells a tree in the woods, it doesn't make a sound. I wouldn't discount the possibility, though, that a future "creative" computer manages to produce a proof indecipherable to humans of a theorem we care about, at which point I think there will be quite a perturbation in the mathematical community. If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved?
补充“智能/创造力”的定义随机械化而漂移，机器的“直觉”一旦可解释就不再被视为直觉
谈论这类 AI 问题时概念很难理清：我们事先称为“智能”的东西，通常是我们想象不出如何机械化的东西；一旦被机械化，我们就不愿再称之为 AI。“创造性”也一样。人类做数学时凭直觉寻找有趣的定理，我们并不理解这种直觉是什么。如果计算机做到了，我们能看清其机制，它大概就不会像直觉了。
netcan查看英文原文
Computers are used more and more but do not play a creative role It's always difficult to get concepts straight when talking about any of these AI-ish questions. The thing that we describe before the fact as "intelligence" is generally stuff we can't imagine mechanizing. Once it is mechanized, and we see the mechanic we don't really like to call it AI. I think it's the same issue for "creative." When humans do mathematics they look for theorems that are interesting intuitively. We don't really understand what this intuition is. If a computer does it, say along the way to solving some other problem, we will be able to look into the mechanic and it probably won't seem like intuition to us.
补充补充资料：ACL2 和 Coq 已有机器学习与定理证明结合的实践
在机械定理证明方面，ACL2 已将机器学习集成进系统（见 arXiv:1404.3034），Coq 也有机器学习插件（arXiv:1410.5467）。
zitterbewegung查看英文原文
For mechanical theorem proving there is ACL2 which integrates machine learning into the system. See http://arxiv.org/abs/1404.3034 also Coq has machine learning add ons http://arxiv.org/abs/1410.5467
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2015Hacker News 讨论帖175 分 · 101 评
同领域还值得读
一种新的相关系数
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 分钟编辑精选