使用20个并行运行的Codex账户解决20个Erdős问题

# Star Fleet Math 来源：https://www.starfleetmath.com/ ## 提议的解决方案\(27\) 许多被列为“开放”的问题已经存在非正式或部分答案在线；我们极力避免处理任何此类问题。 - 1\)Erdős Problem #123 Erdős Problem www.erdosproblems.com/123 (https://www.erdosproblems.com/123) ›问题设 \(a,b,c \ge 1\) 为两两互质的三个整数。是否每个足够大的整数都可以表示为形如 \(a^k b^l c^m\)（\(k,l,m \ge 0\)）的不同整数之和，且这些整数互不整除？（Erdős Problem #123 — 奖金：$250 — 数论 — https://www.erdosproblems.com/123） ›结果对于每一组两两互质的整数 \(a,b,c>1\)，每个足够大的整数都可以表示为不同的 \(a^i b^j c^k\) 项之和，且没有一项整除另一项。在 Lean 中，这是定理 Erdos123.erdos_123 : Erdos123.IntendedStatement。 `` def IntendedStatement : Prop := ∀ a b c : N, 1 < a → 1 < b → 1 < c → PairwiseCoprime3 a b c → IsDComplete (Smooth3 a b c) /-- Erdős Problem 123 针对预期的非退化假设 `a,b,c>1`。 -/ theorem erdos_123 : IntendedStatement := intended_erdos_123 `` ›报告## 解决 Erdős Problem 123 ## 问题及为何常规归纳法失败 对于两两互质的整数 \(a,b,c>1\)，考虑形如 \(a^i b^j c^k\)（\(i,j,k \ge 0\)）的数。问题询问是否每个足够大的整数都可以表示为这些数的不同之和，并额外要求**所选的加数互不整除**。可除性条件是真正的困难来源。通常的完备性论证可以使用来自不同尺度的许多项，但来自不同尺度的项往往可通过可除性进行比较。相反，选择作为可除性反链的集合在算术上可能过于稀疏，无法填充连续整数。 早期工作已经发展出一个强有力的归约方案：选择一个校正项使其模某个基数为所需余数，减去它，除以该基数，然后归纳。对于特定的三元组，这在有限计算机检查后成功。然而，在一般情况下，它留下了一个顽固的**有限种子问题**：必须首先表示一个乘法宽区间 \([N, CN]\) 内的每个整数。校正归纳法并不能构造该区间；它只能传播它。 这解释了为什么一些有吸引力的部分思路未能完成该问题： - 差值为 1 的带符号恒等式给出了两个连续的和，但每类一个余数代表必然具有至少模数减一的跨度。宽度为 1 的区间无法在通常的余数粘合下增长。 - 原始水平上的完全剩余系可以解决同余问题，但对其数值跨度没有说明。 - Van der Waerden 和 Hales–Jewett 论证可以产生原始和上的任意长算术级数，但初始具有不受控制的公差。 - 即使固定了公差，形如 \(B_0 + r d\) 的级数带有一个大的正基线 \(B_0\)。复制这样的级数会以相同速率增加宽度和基线，因此不一定能产生归纳所需的乘法宽种子。 重要的教训是：**大的加法宽度是不够的**。下端点必须保持在定量控制下。 ## 齐次水平坐标系 第一个结构简化是在一个齐次指数水平 \(i+j+k=D\) 上工作。对于大于 1 的两两互质基数，单项式的可除性是指数的坐标比较。因此，同一水平上的两个不同单项式永远不会互相整除。齐次水平的每个子集自动是原始的。这将该问题转化为关于子集和的加法问题，同时使原始性基本上自动满足——只要构造的所有部分可以放在同一个精确次数上。 一种边码构造在一个水平上提供了 \(c^n\) 个原始子集和，具有模 \(c^n\) 的不同余数和有界进位。通过对该进位进行着色并应用 Mathlib 的 Hales–Jewett 定理（本身取自该定理），可以得到原始齐次子集和的任意长精确算术级数。 ## 将一个 AP 转化为大格点区间 将基数排序为 \(10v>0\) 使得 \(2b a^v \le c^v\)。定义两个互质的齐次平移权重 \(A=a^{u+v}, \qquad B=b^u c^v\)。一个 AP 数字族的多份拷贝由权重 \(A^{M-r} B^r\) 平移。选择 \(u>H+1\) 将不同的拷贝放置在不同 \(b\) 指数的分离带中。将每一项乘以 \(abc\) 使得每个 AP 项都是严格内部的。所有拷贝然后位于一个精确指数次数上。一个有界齐次进制引理证明系数和 \(\sum_{r=0}^{M} s_r A^{M-r} B^r, \quad 0 \le s_r < 4AB\) 包含一个宽度至少为 \(2AB^{M+1}\) 的完整区间。将每个系数替换为对应的 AP 数字集，这在一个步长为 \(abcd\)（其中 \(d\) 是 AP 公差）的格点上实现了一个区间。 ## 用面校正填充余数 下一个成分在**每个足够高的精确次数**上，为模任意给定模数的每个余数构造一个原始校正。这些校正支撑在三个坐标面上，并且在有序情况下，其总大小有界于 \(C_{\mathrm{corr}} c^D\)。将此应用于模数 \(abcd\)，在与 AP 进制构造相同的精确次数上。面支撑的校正与严格内部的 AP 项不相交。此外，\(\frac{B}{c^{u+v}} = \left(\frac bc\right)^u > 1\)，因此指数支配给出 \(C_{\mathrm{corr}} c^D = o(B^M)\)。因此校正在宽度上最终小于进制宽度。余数粘合将格点区间转化为一个普通的连续区间 \([L_M, U_M]\)，满足 \(abc B^M \le U_M - L_M, \quad L_M \le K B^{M+1}\)，其中 \(K\) 是固定常数。至此已获得一个真正的区间，但其乘法宽度仍然仅受常数限制。这正好是早期基线问题所在之处。 ## 关键突破：可选的内部壳层 决定性的想法是利用尚未使用的单项式，位于**相同的齐次水平**上。对于线性多个指标 \(s\)，固定一个 \(b\) 指数正好超过所有 AP 带。在剩余的 \(a, c\) 指数中，选择几何网格 \(b^s a^{R-k} c^k\) 中大小低于目标 \(c^{vM}\) 的最后一点。由于连续网格点相差固定因子 \(c/a\)，选定的单项式位于一个受控的乘法窗口内。在恢复公共因子后，这产生了至少 \(M - O(1)\) 个不同的可选单项式 \(z\)，满足 \(z \le X, \quad aX \le cz, \quad X = abc B^M\)。因此每个可选项不大于已存在的区间宽度。可选地添加这样一个项（使用或不使用）会扩展连续区间而不改变其下端点。由于所有可选项仍位于同一精确水平且超出 AP 指数带，原始性和不相交性得以保持。它们的总体贡献是 \(\Omega(M B^M)\)，而下端点仍为 \(O(B^M)\)。因此上端点与下端点的比值随 \(M\) 线性增长。对于每个要求的 \(R>1\)，且超过每个要求的下阈值，这构造了一个原始表示的区间 \([N, RN]\)。这个内部壳层放大正是去除有限种子障碍的方法。成功的坐标变化不仅仅是“在齐次水平上工作”，而是“将主要增长沿一条内部齐次射线放置，然后使用未使用的横向条带作为可选质量”。 ## 完成归纳 余数归约论证被加强为一个灵活的有限种子门：存在常数 \(N_0\) 和 \(C>1\)，使得**任何**已表示的区间 \([N, CN]\) 当 \(N \ge N_0\) 时蕴涵 \(d\)-完备性。对 \(R=C\) 应用任意宽度构造证明了有序基数 \(11a,b,c>1\) 的猜想，这些猜想在源文献中以及独立的形式猜想编码中使用。 ›下载完整解决方案 & 用你的 AI 验证 - 2\)Erdős Problem #129 Erdős Problem www.erdosproblems.com/129 (https://www.erdosproblems.com/129) ›问题设 \(R(n;k,r)\) 是最小的 \(N\)，使得如果将 \(K_N\) 的边进行 \(r\) 染色，则存在一个 \(n\) 个顶点的集合，在该集合上至少一种颜色不包含 \(K_k\)。证明存在常数 \(C=C(r)>1\) 使得 \(R(n;3,r) < C^{\sqrt{n}}\) 对所有 \(n\) 成立。（Erdős Problem #129 — 图论、Ramsey 理论 — https://www.erdosproblems.com/129） ›结果存在常数 \(C>1\) 使得 \(R(n;3,2) < C^{\sqrt{n}}\) 对所有 \(n\) 成立。因此精确的形式命题 LiteralProblem129 为假。 `` theorem not_literalProblem129 : ¬ LiteralProblem129 := by intro h exact not_claimedBoundFor_two (h 2 (by omega)) theorem R3_two_global_exponential_sandwich (n : N) (hn : 120 ≤ n) : 2 ^ (n / 120) < R3 n 2 ∧ R3 n 2 ≤ 2 ^ (2 * n) := by exact ⟨two_pow_div_120_lt_R3_two n hn, R3_two_le_two_pow_two_mul n⟩ `` ›报告## Erdős Problem 129：一个经过形式化验证的反驳 ## 问题及为何具有欺骗性 Erdős Problem 129 定义了一个 Ramsey 型阈值 `R(n;3,r)`：最小的阶 `N`，使得 `K_N` 的边的每个 `r` 染色都有一个 `n` 个顶点的集合，在该集合上至少一种颜色不含三角形。提议的界是 `R(n;3,r) < C(r)^{\sqrt{n}}`。初看这像是多色 Ramsey 理论中的一个困难上界问题。还有一个额外的历史障碍：现代的 Erdős 问题数据库已经记录了 Antonio Girão 的观察，即所显示的陈述是假的，但对 1997 年来源可能意图某个不同、未陈述的定义仍保留了“开放”标签。这种模糊性很重要。反驳一个误转录并不能解决意图中的问题，而默默地发明一个替代方案也不会回答已发布的问题。因此这项工作必须同时解决数学问题和陈述忠实性问题。 ## 早期推理遗漏了什么 决定性的概率估计来自于考察**每个测试顶点集内部的许多边不相交三角形**。一个随机的红蓝染色使得任何固定三角形在指定颜色上成为单色的概率为 `1/8`。如果一个 `n` 集包含二次多个边不相交的三角形，这些事件使用不相交的边变量并且独立。因此，该集合在指定颜色中没有三角形的概率在 `n^2` 上是指数小的，而不仅仅在 `n` 上。这足以对阶为 `n` 的指数级大小的图的所有 `n` 子集进行并界。因此打印的 `exp(c√n)` 下界仅仅是一个弱真下界；它与已发布定义逻辑一致，并且不强制存在缺失条件。 还有两个形式化死胡同： - 一个初始计数证明使用了 Lean 的 `native_decide`。虽然计算上正确，但这引入了生成的公理，不适合仅内核的证书。它被替换为内核 `decide`。 - 第一个端点否定了操作上的最小阶表述，而形式陈述使用自然数下确界定义了 `R`。这个差距需要有限 Ramsey 定理和证明下确界可达。 ## 可行的构造 对于每个参数 `t≥1`，取任意一组 `60t` 个顶点，并将其分成三个相等的部分。形式为 `(i, j, i+j)` 的拉丁方三元组产生一个二次族的成对边不相交三角形。形式构造为集合的每个枚举提供 `6(60t^2+2)` 个这样的三角形。对于一种目标颜色，避免单色填充三角形的染色最多有 `7^L · 2^(|E|-3L)` 种可能性，其中 `L` 是填充大小。对两种颜色和所有枚举的 `60t` 集进行并界证明，`K_{2^t}` 的某种染色使得**每个** `60t` 集同时包含一个红三角形和一个蓝三角形。因此 Ramsey 性质在环境阶 `2^t` 上失效。这已经击败了所有平方根指数上界。 为了确定实际尺度，一个初等规范序列证明给出了互补的有限 Ramsey 估计 `R(n;3,2) ≤ 2^(2n)`。测试集大小的单调性将填充下界从子序列 `n=60t` 扩展到每个 `n≥120`：`2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n)`。所以字面阈值是线性指数的，而猜想的上界只有指数 `√n`。 ## 解决来源模糊性 直接检查了 Erdős 1997 年论文的出版商扫描件。它定义 `f_k^{(r)}(n)` 为允许一个 `r` 染色的最大阶，使得每个 `n` 集在每种颜色中都包含一个 `K_k`。Lean 证明，对于 `k=3` 和两种颜色，这个可允许条件正是网站上 Ramsey 谓词的否定。然后调查遵循了历史替代方案，而不是假定扫描件是结论性的： - Erdős 和 Gyárfás 的 *Split and balanced colorings of complete graphs* 定义了不同的最小阶分割和平衡参数，其行为是指数多项式而不是平方根指数。 - 他们的 *A variant of the classical Ramsey problem* 研究了 `(p,q)` 染色和一个不同的极值函数。 - Gyárfás 2013 年的回顾讨论了这两个项目，但没有给出 Problem 129 的修正版本。 - 对 Gyárfás 出版页面上链接的所有 218 个 PDF 的可搜索语料库进行检查，未发现后来的修正或替代表述。 因此，来源的弱概率下界并不识别另一个问题，也没有主要来源提供一个。形式化验证的反驳回答了唯一确定已发布的陈述。Girão 保留了初等概率反对的优先权；这里的贡献是完整的形式证书、精确阈值诊断和来源审计。 ## 验证 该证明是一个独立的 Lean 4 + Mathlib 项目。它包括： - 边染色、单色三角形、`RamseyAt` 和精确下确界 `R3` 的忠实定义； - 拉丁方三角形填充和精确染色计数； - 并界构造； - 环境阶和测试集大小的单调性； - 有限 Ramsey 存在性和下确界可达性； - 所提议定理的精确否定和全局指数夹逼。 验证器构建所有 8572 个目标，直接检查最终定理文件，并拒绝 `native_decide`、`sorry`、`admit` 或任何声明的公理。最终定理仅依赖于 Mathlib 的标准逻辑原则 `propext`、`Classical.choice` 和 `Quot.sound`。 `` cd verified_math/F-015_global-exponential-threshold/lean && bash verify.sh `` 运行结束于： `` Build completed successfully (8572 jobs). PASS: global exponential sandwich kernel-checked; no forbidden proof escape `` ›下载完整解决方案 & 用你的 AI 验证 - 3\)Erdős Problem #130 Erdős Problem www.erdosproblems.com/130 (https://www.erdosproblems.com/130) ›问题设 \(A \subset \mathbb{R}^2\) 是一个无限集合，其中无三点共线且无四点共圆。考虑以 \(A\) 中的点为顶点的图，当且仅当两点间的距离为整数时连边。该图的色数和团数可以有多大？特别地，色数可以是无穷大吗？（Erdős Problem #130 — 图论、色数 — https://www.erdosproblems.com/130） ›结果存在一个无限集合 \(A\) 在 \(\mathbb{R}^2\) 中，不含三点共线且不含四点共圆，使得对于每个自然数 \(k\)，连接正整数距离对的图。