Erdosproblems

Erdős 问题集，收录 Paul Erdős 及其合作者提出的数学问题，追踪问题的解答进展与悬赏状态。

GPT 5.6 Pro 声称证明埃尔德什素数间隙猜想

GPT 5.6 Pro 在 Erdős Problems 网站提交了一份关于素数间隙的证明，声称解决了埃尔德什提出的经典问题：对任意常数 C，存在无穷多个相邻素数间隙大于 C·log(p_n)·log(log(log(p_n)))/log(log(p_n))。该证明由用户 DottedCalculator 提交，页面明确标注"提交不代表正确性"。Maynard 和 Ford-Green-Konyagin-Maynard-Tao 此前已在此方向取得重要进展，当前最佳下界约为 exp(c·log log log x / log log x)。 AI 能否真正解决重大数学猜想，仍是待验证的开放问题。

收藏30 天前

和积集、单位距离与数域

数学家Thomas Bloom以亲身参与者视角，详解近期实数域上单位距离猜想与和积猜想的反例构造。核心看点：这不是泛泛的科普，而是参与构建反例的数学家亲自拆解思路。作者从"张量积技巧"热身问题出发——如何将小常数放大为任意大的指数改进——引出核心策略：先找一个小常数改进，再通过高次数域放缩。随后清晰勾勒代数数论关键工具：整数环构成高维格点（判别式控制体积）、单位群通过对数嵌入成为另一个格点（调节子控制体积），两者通过类数公式关联。和积反例利用Martinet的数域塔使判别式可控，取加法球与乘法球的交集构造集合；单位距离反例则利用二次扩域中单位群的结构构造大量等距点对。全文强烈个人色彩：作者坦言自己一个月前还不太懂代数数论，边学边写，明确邀请读者评论纠错。对于有数学背景的读者，这是不可多得的"insider视角"解读。

收藏121 天前

GPT-5.4解决重大开放数学难题——陶哲轩与Jared Lichtman评论

GPT-5.4 Pro在提示下证明了Erdős原始整数集猜想（#1196），该猜想已存在40余年。菲尔兹奖得主陶哲轩、问题研究者Lichtman等人在Erdős问题论坛展开深度技术讨论，解析证明中von Mangoldt流方法、对偶证书构造与不变测度等关键创新。陶哲轩指出AI"幸运地"找到了唯一可行路径，并对比了其他方案为何失效。多位数学家贡献了变体方案、误差项改进和后续扩展方向。这是AI独立解决重要开放数学问题的最新里程碑，讨论本身也展示了顶尖数学家如何看待和参与AI辅助的数学发现过程。

收藏162 天前

埃尔德什 #1051 问题获证：AI 智能体发现证明已完成 Lean 形式化验证

AI 智能体（Gemini Deep Think）自主发现并完成了埃尔德什 #1051 问题的证明，且在 Lean 中通过形式化验证。该问题探讨整数序列增长条件与级数无理性的关系：若整数序列增长速度快于黄金比例，则其倒数级数必为无理数；反之可构造反例。 Barreto、Kang、Kim、Kovač 和 Zhang 给出了近乎完整的充要刻画，Aletheia 也独立证明了原问题。这是典型的人机协作数学前沿案例——AI 负责发现，人类补充延伸，形式化工具确保严谨性。

收藏242 天前

Erdős问题#347被解决（AI辅助数学证明）

Erdős未解决问题#347被网友破解，陶哲轩亲自参与讨论，证明已通过Lean形式化验证。问题询问是否存在整数序列，使每个余有限子序列的子集和密度均为1。网友ebarschkis基于陶哲轩与Woett的思路给出构造性证明，并用Lean完成了完整形式化验证（Lean v4.24.0）。陶哲轩本人在帖中贡献了另一种基于Woett思想的构造思路，将问题与Graham经典结果关联讨论。这不是一篇普通新闻稿，而是数学社区围绕一个开放问题的真实协作记录——有完整的论证草稿、Lean代码、多轮讨论和不同解法比较。对数论爱好者、Erdős问题追踪者和形式化验证关注者，是一手材料丰富的深度内容。

收藏251 天前

埃尔德什问题 #281：覆盖系统密度与形式化验证

埃尔德什经典数论问题#281的讨论帖，问题涉及同余覆盖系统的密度充分性条件。该问题近期已被肯定解决，且证明已在Lean中完成形式化验证。讨论中有多条高质量评论：Terence Tao提供了Rogers定理证明的博客链接；Neel Somani借助ChatGPT给出了一个证明；KoishiChan则提供了基于Davenport-Erdős定理的另一种初等证明。评论特别指出，该证明思路在1980年对Erdős本人而言本应十分自然却被遗漏，颇具历史趣味。页面还列出了28条论坛讨论。适合对解析数论、覆盖系统或Lean形式化验证感兴趣的读者。

收藏255 天前

GPT 5.2 协助解决埃尔德什 #728 数论难题

GPT-5.2 参与解决了埃尔德什（Erdős）#728 开放数论问题——关于阶乘整除性与二项式系数可除性的深度猜想。Nat Sothanaphan 在讨论帖中详细记录了与 GPT-5.2/ChatGPT 协作完成证明、写出完整论文并提交 arXiv 的全过程，包括 Lean 形式化验证的细节。陶哲轩（Terence Tao）亲自参与讨论，比较了人类顶级数学家（Pomerance）与 AI 在证明思路和写作风格上的差异，指出双方思路高度相似但表达方式不同。帖子还深入讨论了 AI 辅助数学研究的真实工作流（AI 擅长写证明细节但需要人类严格把关）、Pomerance 独立证明与 AI 证明的逐项比较、以及是否将 AI 协作成果投稿期刊的伦理与学术争议。这是 AI 协作攻克经典开放数学问题的一次罕见的实时完整记录，对关注 AI 能力边界和数学研究未来方向的人极有阅读价值。

收藏266 天前

Harmonic数学AI "亚里士多德" 解决了一个埃尔德什难题

核心看点：Harmonic 的数学 AI "Aristotle" 仅用 6 小时，独立证明了一个埃尔德什公开问题（#124），并在 Lean 中完成了形式化验证。该问题涉及整数能否表示为若干不同幂次之和的充要条件，此前由 Erdős、Burr、Graham、Li 等人提出并部分研究。AI 给出的证明"出奇地简单"，从形式化陈述出发，无需人类提示。页面还记录了问题陈述中的打字错误、学界对 gcd 条件的讨论、Tao 的评论，以及 Melfi 等相关构造结果。这是一个 AI 在纯数学推理上取得实质性突破的真实案例，而非营销包装。

收藏303 天前

来自Harmonic的Aristotle解决了这个Erdős问题

AI系统Aristotle独立解决了Erdős #124数论开放问题，解答出人意料地简洁。该问题由Erdős本人提出，探讨能否将充分大的整数表示为特定不同幂次之和，长期悬而未决。 Aristotle仅从形式化陈述出发，6小时内独立给出证明，Lean形式化验证仅耗时1分钟。文章包含完整问题陈述、历史沿革（BEGL96论文、Melfi构造等）、AI求解过程、形式化表述中的笔误争议，以及社区对证明细节的讨论（核心思路是将幂次序列排序后验证部分和条件）。内容兼具数学深度与AI解决开放问题的新闻价值。