Meta用一道除法教AI“搞数学研究”!顶尖数学家当场发飙:看完我想吐

2026年9月，数学界和AI圈突然爆发了一场毫无预警的正面大火拼。

加州大学伯克利分校数学教授、Google DeepMind研究科学家Tony Feng直接在社交媒体上公开发难：

“看到这篇论文对‘有趣’下的定义，我恶心到嘴里直泛酸水。”

▲ 加州大学伯克利分校数学教授Tony Feng发推怒批：把这种定义写进论文，AI研究员问过数学家吗？

究竟是什么让一位顶级数学家如此失态？

惹事的，是来自Meta FAIR实验室、纽约大学与巴黎路桥学院（ENPC）的一篇重磅arXiv预印本论文《学会发现有趣的数学》（Learning to Discover Interesting Mathematics）。

领衔这篇论文的，是AI巨擘Julia Kempe以及Niket Patel等一众学者。他们宣布：AI不仅会做数学证明题，现在还能自主提出“有趣的数学猜想”了！

而他们教AI理解“什么叫有趣”的核心秘诀，竟然只是一道小学生都能看懂的除法公式。

01一道除法公式，掀翻了数学家的祖师殿

这篇论文到底写了什么？

简单来说，作者团队给数学命题的“内在有趣度”（Interestingness）设计了一个极其粗暴的数学量化指标：

有趣度 ≈ 证明难度（代码行数） ÷ 陈述长度（代码行数）（也就是：“容易陈述、难于证明”的命题得分最高）

▲ Meta FAIR等机构学者发布新论文，提出利用标量信号量化数学“有趣度”

在计算机科学家眼里，这个逻辑堪称绝妙：

• 费马大定理
  ：$x^n + y^n = z^n$ 在 $n > 2$ 时没有正整数解。一句话，中学生都能听懂（分母极小）；人类却耗费了350年、写了几百页现代代数几何才证出来（分子极大）。得分爆表，极其有趣！
• 平凡恒等式
  ：比如 $1+1=2$ 或者各种无聊的逻辑代数展开。说起来废话连篇，证明只需一行。得分垫底，毫无趣味！

团队不仅提出了这个定义，还以此为奖励信号，用 GRPO（群相对策略优化） 算法后训练了一个27B规模的数学猜想生成模型。

为了防止训练时“每提一个猜想都要证半天”导致算力崩溃，他们甚至先训练了一个 27B的价值函数模型，不写证明，光看题目陈述和已知公理，就能预测证明难度。论文数据显示，这个价值模型对证明难度的预判准确率，直接超越了GPT-5.5和Claude Opus 4.6。

最终实验结果更是亮眼：猜想生成模型的真实验证有趣度均值从1.76飙升到了7.58，足足暴涨4.3倍；而且它生成的猜想中，与现有数学库重复的比例从91.9%暴跌到了30.6%。

AI学会避开人类抄过的作业，开始自主走向未知的数学荒原。

02圣杯争夺战：从“做题家”到“探险家”

要看懂这场冲突，我们必须先退一步，看看数学AI正卡在怎样的瓶颈上。

今天的数学AI，能力其实分成了泾渭分明的三层：

第一层是自然语言解题大模型像考生一样在草稿纸上写步骤，逻辑可能漏洞百出，还会一本正经地“胡说八道”。

第二层是形式化机器证明人类把命题翻译成 Lean 这种由底层内核严格校验的计算机语言。目前全球最大的形式化数学标准库 mathlib，已经积累了数百万行无懈可击的代码。在这层战场上，AlphaProof 拿下了国际数学奥林匹克（IMO）银牌水平，DeepSeek-Prover 等系统也在不断刷榜。

但走到这里，所有AI顶尖团队都撞上了一堵高墙，第三层：选题与发现。

▲ 纽约大学教授、论文共同作者Julia Kempe直言：AI定理证明的圣杯远不止堆砌真命题，核心在于自主发现新数学

法国数学巨擘庞加莱曾留下一句名言：“事实的堆积并不比一堆石头更成其为科学。”

阿根廷作家博尔赫斯笔下那座令人绝望的《巴别图书馆》也是同理：如果一座图书馆里理论上藏着全宇宙每一句真理，但99.9999%的内容都是 $A=A$ 这样的纯粹垃圾废话，那这座图书馆就毫无意义。

如果只给AI配备强大的证明器，AI就会化身一台不知疲倦的“废话制造机”：它能在一秒钟内生成并证明数亿条诸如“若A为真且B为真则A为真”的真命题。

在无限的真理海洋里，谁来告诉AI，哪一颗贝壳才闪烁着珍珠的光芒？

Julia Kempe团队的野心正在于此：他们试图给AI装上一双“数学品味的眼睛”，让它自己挑题目、自己证、自己把证出来的结果作为地基，去冲击下一座高峰。

03数学家的毒舌：圆周率反例与望月新一的啤酒

但这个在计算机学者看来极具工程美感的公式，却直接踩中了职业数学家最敏感的神经。

Tony Feng在社交媒体上毫不客气地补刀：这种把“证明长/陈述短”当成有趣的设想，数学圈私下讨论过无数次，每次都是当场被扔进垃圾桶。“令我惊讶的是，AI研究员居然有胆量把它奉为正典写进论文里！你们在定义什么是‘有趣的数学’之前，就不能先去问问职业数学家吗？”

批评的声音迅速在学术圈蔓延开来

最诛心的反驳，来自研究者Jack McCarthy抛出的一个经典构造反例：

▲ Jack McCarthy提出经典反例：超高精度圆周率计算，命题极短、证明极难，却毫无价值

请看这个命题：“圆周率 $\pi$ 的第 $10^{10^{10^{10}}}$ 位数字是 3。”

• 陈述长度
  ：极短，十几个字符。
• 证明难度
  ：目前全人类的超级计算机加起来都算不出来，证明步骤可能需要数亿行代码。

按照Meta的公式，这个命题的“有趣度”直接突破天际，堪称人类数学皇冠上的明珠！但任何一个心智正常的数学家都会告诉你：这纯粹是一个毫无理论价值的无聊垃圾。

更有网友搬出了数学界的知名公案玩梗：日本数学家望月新一号称证明了abc猜想，甩出了五百多页晦涩难懂的长篇巨著，至今数学界无法完全达成共识。网友笑称：“望月新一看到这篇论文怕是要说：‘小老弟，帮我拿一下啤酒，我的论文有趣度天下第一！’”

甚至连作者团队的“前科”也被扒了出来，2026年5月，同一帮作者发布了号称将数十本教材自动形式化进Lean的ATLAS项目，当时就曾被社区质疑存在为了刷量而过度简化、曲解原著意图的硬伤，被一些数学家戏称为“史上最大的形式化翻车现场”。

04降维打击还是盲人摸象？两种文明的剧烈碰撞

面对铺天盖地的嘲讽，论文一作Niket Patel迅速出面回应：团队成员本身都受过严格的数学训练，论文从未狂妄到声称这个公式代表了人类数学审美的全貌。

前Google研究员、形式化数学领军人物Christian Szegedy以及数学家Eric Naslund等人也纷纷下场拉偏架：在强化学习的世界里，一个粗糙但能够计算、能够跑通闭环迭代的标量信号，哪怕有缺陷，也比空谈所谓不可名状的“人类崇高审美”有用一万倍！

▲ Niket Patel回应同行争议：团队深知局限性，量化指标旨在为机器探索提供可计算的抓手

这场论战早已超出具体的公式对错，本质上是两种科研文明在最高维度上的激烈撞击：

• 传统数学家的范式，是“自上而下”的意境流
  。数学的“有趣”，在于它是否连接了两个看似毫不相关的遥远领域（如数论与几何），在于它是否开创了一整套全新的概念工具箱，在于那份只可意会不可言传的结构对称与精神震撼。
• AI与机器学习的范式，是“自下而上”的工程流
  。计算机唯一的指挥棒就是损失函数（Loss Function）。只要给不出一个具体的数字，梯度下降就无法发生，机器便寸步难行。

这就像互联网早期的产品经理用“点击率（CTR）”来定义文章质量，或者软件工程用“代码行数”来考核程序员一样，数学家们一眼就能挑出无数个荒谬的极端Bug，但这并不妨碍这个简陋的指标，成为推动庞大工程机器运转的第一颗齿轮。

05终局：从学徒走向旷野

尽管伴随着巨大的争议，我们仍然不得不承认这篇论文所折射出的历史转折点。

过去五年，数学AI一直在扮演一个顶级的“应试学生”：人类把出好的IMO考题、前沿猜想喂给它，它绞尽脑汁在算力海洋里搜索答案。

而从这项工作开始，AI正在尝试迈出摆脱“人类投喂”的第一步。

通过这个单薄却可优化的公式，模型在八个数学领域里，自主筛选出了一批诸如“单位纯虚四元数刻画-1的平方根”、“上半平面指数衰减”等具有非平凡结构的新定理。虽然离孕育出下一个“相对论级别的数学体系”还差了十万八千里，但它已经不再是一台只会把同一个公理翻来覆去倒腾的复读机。

▲ 自我扩展的数学发现闭环：生成，证明，排序，晋级，重复

庞加莱说得没错，科学绝非石头的简单堆叠。

但要建造宏伟的数学大厦，首先得有人教会挖掘机，怎样在一整座大山里，辨认出哪一块是坚硬的花岗岩，哪一块是无用的烂泥巴。

AI对人类“品味”的拙劣模仿，或许在今天看来还漏洞百出、令人发笑；但当它真的在无人指引的旷野里，开始尝试搬起第一块有分量的基石时，人类数学家们，真的准备好迎接这位同伴了吗？