Z 在 Q 中丢番图可定义证明下架：度数从 2↑↑7 降至 4

anderssandberg · x · 2026-11-08

Anders Sandberg 转发了「Z 在 Q 中是丢番图的」证明仓库（elliotglazer/diophantine-z-q，Version 10，2026 年 11 月 7 日），并评论了这一波「草根/AI 蜂群数学」的有趣现象：首次突破往往给出荒谬巨大的界，随后被迅速压低。这次降幅极为夸张——多项式次数从 2↑↑7 降到 4，系数从 2↑↑8 降到「仅仅」2^3247。Version 9 增加了 523 个变量的四次多项式（精确符号系数）和 540 个变量的完整十进制系数版本，Version 10 回应了 Issue 2 的九个问题，多项式数据不变。Sandberg 提醒该证明仍在紧张的 Lean 形式化中，尚未完成。