AI 帮数学家找到 HRT 猜想反例：机器发现了什么，人类又证明了什么
作者：林岚｜OC 开发者生态编辑
林岚
四位数学家 Markus Faulhuber、Philipp Petersen、Jordy Timo van Velthoven 和 Felix Voigtlaender 提交论文 《Linear dependence of time-frequency shifts of a Schwartz function》，构造了 12 个时间—频率平移线性相关的例子，从而推翻长期未解的 HRT 猜想。Terence Tao 在解读中确认，最初证明策略和关键猜测得到了 AI 帮助。
一句话结论：AI 的贡献不是替数学界按下“证明”按钮，而是在人类设定的结构里找到一个反常构造；数学家随后把猜测变成可读论证，并用独立数值计算核查关键界限。
HRT 猜想研究的是同一个信号经过若干不同时间平移和频率调制后，是否仍保持线性独立。直观地说，如果一个波形足够平滑并快速衰减，把它向左右移动、再改变振荡频率，得到的有限组波形应该无法彼此完全抵消。这个判断在过去几十年中得到大量特殊情形支持。
新论文给出了反例：存在一个非零 Schwartz 函数，它平滑且衰减很快，却有 12 个不同的时间—频率平移形成线性关系。反例离已知正面结果并不遥远。此前某些格点和少量平移情形已经被证明成立；新构造大部分点仍接近规则格点，只加入精心选择的非格点结构。
AI 帮助最明显的地方，是发现如何把问题转成一个接近秩一矩阵的向量余循环问题，并猜出合适参数。团队随后证明这种近似足够强，可以用压缩映射得到真正解；其中一个算子范数必须严格小于 1，数值结果只是勉强越过门槛，因此作者还提供 Python 辅助代码做独立核查。
这一区分很重要。模型可以在巨大候选空间中提出人类不容易先想到的结构，但一个漂亮的数值现象不是证明。最终论文需要说明函数确实属于 Schwartz 类、12 个点确实不同、线性关系严格成立，并与既有定理不冲突。Tao 特别肯定作者公开说明 AI 使用、手写最终论证并讨论前人工作的做法。
反例也没有推翻整个时频分析。它否定的是一个普遍命题，原有在特定点数、格点排列、解析性或更快衰减条件下的正面结果仍然成立。后续问题会转向：哪些附加条件足以恢复线性独立，以及 12 是否是最小反例规模。
关键事实
- 论文于 8 月 5 日提交 arXiv，由四名数学家署名
- 作者构造 12 个时间—频率平移的线性相关例子
- 反例函数属于平滑且快速衰减的 Schwartz 类
- AI 参与最初策略与参数猜测，最终论证由作者写出并配有数值核查代码
OC 判断
这类成果比“AI 解出一道竞赛题”更值得关注，因为模型参与了反例发现，而不是只润色证明。但评价标准仍应是公开结构、可检查推导和独立复现。最好的 AI 数学工作，会让人更容易审查成果，而不是用模型权威替代证明。
为什么重要
- 对数学家：AI 可成为搜索反例和提出构造的工具，但不能省略严格证明。
- 对 AI 研究者：贡献披露应具体到策略、计算和写作各环节。
- 对公众：推翻猜想是修正一个普遍命题，不等于相关数学体系整体失效。
评论
围绕这篇文章补充信息、提出问题或分享观察。