2026年11月5日，数学研究者 Elliot Glazer 在 GitHub 挂出一篇148页的论文，宣称与 OpenAI 的 Astra、Anthropic 的 Claude 两个模型联手，参与构造了一个拥有约2929亿个变量的整系数多项式。热榜词条里“3000亿变量”的准确数字，其实还没到整3000亿。小红书
论文题目是《Z is Diophantine in Q》：一旦这个构造被验证成立，一个固定的整系数多项式方程就能在有理数里“点名”出所有整数，Mazur 猜想将被直接证伪，希尔伯特第十问题在有理数上也会迎来与整数上一样的否定答案。换句话说，热榜那句“AI 用多项式推世纪难题”，兑现的是两个连在一起的结论。小红书
但先把底线说清：这篇论文没有经过同行评审，也没有机器层面的形式化检查，作者自己也承认目前的证明尚未完成形式化验证。它仍是一份“声称”，只是这次摆出来的可查零件，明显比几个月前足。小红书
百年难题卡住的从来不是“解方程”，而是“有没有万能判定法”
希尔伯特在1900年抛出这个问题时，问的不是怎么解某个具体方程，而是一个更冷的问题：存不存在一种算法，输入任意整系数多项式方程，就能判定它有没有解。整数上的答案早已是明确的否定——这样的算法根本不存在。而真正的难点在于把否定答案搬到有理数：数学家长期追问的其实是一步地基——能否通过一个多项式方程，在有理数范围内精确识别出所有整数？因为除非整数先被“圈”进有理数的世界，整数的不可判定性才装得进有理数的问题里。小红书小红书
这个“能不能圈出来”，正是 Barry Mazur 的著名猜想断言“不可能”的方向。而 Glazer 声称恰好把它构造了出来：若证明成立，整数集在有理数上可丢番图定义，这个猜想也将被推翻。小红书
今年这条线不止一次松动。9月底，一篇发表于《数学新进展》的论文把希尔伯特第十问题在任意数域整数环上无条件解决——但整数环终究是“整数味”的，最刺眼的空缺始终是有理数域本身这一格。 10月，OpenAI 那份722手稿清单把有理数版本列为第004号问题，给出的同样是声称级别的结论：不存在通用算法。 同月，研究者 Sohail Farhangi 又用 ChatGPT 6 Pro 交出一份还挂着前提的证明。 Glazer 这次的区别在于：他给出的是一条不依赖额外猜想、直接构造多项式的路。小红书知乎小红书
“约3000亿变量”不是公式很长，而是构造的代价
按论文里的精确表述，这个多项式P有 2929 亿个变量，多项式的总次数小于 2↑↑7，每个系数的绝对值小于 2↑↑8。 双箭头是高德纳幂塔记号：2↑↑7 是 7 个 2 一层压一层地互作指数——这还只是上界，也足以说明为什么没有任何人能把它手写出来逐字验算。所以这次和7月的雅可比猜想反例完全是两类新闻：那是个3变量多项式，普通人几分钟就能重算一遍，公开的 Lean4 文件已经把它形式化验证过。 而这次要检查的不是结论，而是构造本身：148页就是构造链，每一环单独可查，但必须把整条链走完。小红书知乎
至于变量为什么堆到天文数字——这类证明要把一整个判定过程编码进一个多项式方程，编码链条每延伸一段就带入一批新未知数，规模随之滚雪球。这不是 Glazer 的怪癖，而是这条证明路线的通行代价。
AI写证明，AI审证明：踩着10月风波走出来的做法
论文致谢里，作者特意感谢了自己的两位“好朋友”：Astra 和 Claude。 这和7月那句“好朋友Fable帮他找到了反例”如出一辙。 只是这种高调，放到三个月前已经是一把双刃剑。小红书知乎
10月6日，OpenAI 把722篇 AI 生成的数学手稿一次性挂上 GitHub，作者栏只写着 OpenAI 一个词。 第二天，其中3篇就因同一个正负号错误作废。 数学界的反弹随即公开化：人类数学协会（AHM）发布声明，呼吁全球数学家停止与 OpenAI 合作，菲尔兹奖得主陶哲轩在博客转载。微博微博微博
Glazer 显然不希望重蹈覆辙：他让 AI 对论文引用的定理逐项审查，核对假设条件、符号约定和适用范围，并把82项审查记录全部公开挂出。 他还把 Farhangi 的条件性手稿一并收进同一个仓库，准备两份证明对照着比——把一场本可以抢发的竞赛，做成了明牌接力。小红书
现在能信几分，接下来盯什么
先把状态说死：OpenAI 那批成果里，包括ℚ上的希尔伯特第十问题在内，当时就只是声称的证明，尚无任何形式化或同行验证。 Glazer 的论文眼下处于同一种状态，区别只在于他摆出来的可查零件更多。知乎
如果它站住，后果链很干净：整数在有理数上可丢番图定义，于是“判定有理系数方程组有无有理解”的通用算法永远不存在，Mazur 猜想所支持的那批研究方向随之关门。如果它站不住，它就只是“正负号错误”案例库里又多一条——10月的先例也说明，数学界消化这类结果的速度，已经比几个月前成熟得多。
接下来值得盯三个信号：数学家能否独立复核构造链的关键环节；Lean 一类的机器形式化有没有实质进度；Glazer 仓库里这条路线与 OpenAI、Farhangi 两条证明的差异，会不会被公开写清。而对普通读者，一条更省事的判据是：7月以来，“AI解决世纪难题”的热词条只会越来越密，真正该看的不是模型名，而是结果走到“声称—同行评审—形式化验证”的哪一格。这一次的答案：结论未经证实，但可验证性拉满——它停在第一格，只是把检查自己所需的工具，几乎都摊在了桌上。
