如果你还没关注 @imjaredz，现在就该关注了 ——

demonstrandum-research/artifacts

来源：https://github.com/demonstrandum-research/artifacts

Demonstrandum — wave-1 已验证工件

DOI (https://doi.org/10.5281/zenodo.20673864)
代码：MIT 文本与数据：CC BY 4.0
仓库大小 (https://github.com/demonstrandum-research/artifacts)

Demonstrandum 是一个以验证为先的多智能体 AI 数学管线，由 John Erlbacher（独立研究员）指导并审计。其核心规则：不接受任何仅凭 AI 说辞的主张——进步的衡量单位是磁盘上的一个工件，加上一个独立编写的检查器接受该工件。因此，下面的每个结果你都可以机械式地验证，无需信任任何 AI 或作者。

本仓库最初包含完整的 14 个结果的 wave-1 工件包（11 个对已发表猜想的反驳、两个对已发表猜想的证明、一个数值记录），附有六篇论文和一个一键式主验证程序集。现在它还包含了第 15 个结果，即 Erdős 问题 #866 版本（2026-07-08）—— Choi–Erdős–Szemerédi 常数的最终值，对所有 n ≥ 331,777 有 h4(n) = 4，在 Lean 4 中经过核心验证，同时改进了 g5/h5 上界以及一个包含 298 个单元的双引擎 SAT 认证精确值表——以及后续的强多数五色和六色核心包。这些后续包有各自的重新构建说明，不会静默包含在旧版主验证程序集中。

• 精确声明、逐字冻结的陈述、按结果列出的注意事项：RESULTS.md
• 每个检查能做什么和不能做什么（供外部数学家参考的指南）：VALIDATION.md
• 当前包概念 DOI: 10.5281/zenodo.20673864 (https://doi.org/10.5281/zenodo.20673864)；7 月 8 日 v3 快照：10.5281/zenodo.21269439 (https://doi.org/10.5281/zenodo.21269439)
• 强多数五色版本：papers/five-colors/，概念 DOI 10.5281/zenodo.21316623 (https://doi.org/10.5281/zenodo.21316623)
• 强多数六色前身：papers/five-colors/six-color-artifact/
• 联系方式：John Erlbacher — [email protected] — ORCID 0009-0003-6851-4139 (https://orcid.org/0009-0003-6851-4139)

结果等级

在 RESULTS.md 中有精确定义：
kernel = 整个声明是一个 Lean 4 定理，被 Lean 核心接受，仅使用三个标准的 mathlib 公理；
dual-checker = 证书被 ≥ 2 个独立编写的检查器接受，并通过变异测试；
audit-panel = 存储了可运行的检查器，加上跨模型族的对抗性洁净室审计。

每个结果还在 RESULTS.md 中附带了明确的“这未证明什么”的注意事项——声明校准是协议的一部分。

快速开始

要求：Python 3.10+，包含 numpy 和 sympy。包含预构建的 Windows x64 Rust 检查器二进制文件；在其他平台上，当安装 cargo 时会自动重新构建。

git clone https://github.com/demonstrandum-research/artifacts.git
cd artifacts
python verify_all.py                # 默认程序集：33 个检查，约 5-15 分钟
python verify_all.py --full         # 增加长冗余层，约 25-30 分钟
python verify_all.py --strict       # SKIP 变为失败（完全零信任模式）
python verify_all.py --list         # 列出所有检查；--only SUBSTR 运行子集

在没有本地 Lean 构建缓存的情况下，预期的最后一行（两个 Borsuk Lean 检查会给出 SKIP 并附带说明，而不是启动数小时的 mathlib 构建）：

TOTAL: 31 PASS, 0 FAIL, 2 SKIP in ... s
WARNING: SKIPped checks mean the following results were NOT verified on this machine: Borsuk-C3

完成 Lean 构建后（下一节）：TOTAL: 33 PASS, 0 FAIL, 0 SKIP。SKIP 始终意味着“未在此机器上验证”——摘要会明确说明。

论文

六篇 wave-1 论文伴随旧版头条结果。每个目录包含 LaTeX 源码、编译后的 PDF、构建说明（BUILD.md）、审稿回复（RESPONSES.md）和重新计算脚本。

离散 Borsuk — papers/borsuk/note.pdf

对立方体猜想特征的反例。 Brose、De Loera、Lopez-Campos 和 Torres 证明了有界集 S ⊂ Z^d 的格 Borsuk 数至多为 2^d，并猜想（arXiv:2508.20009，猜想 3）当且仅当 conv(S) 单模等价于一个立方体时它等于 2^d。四点集 {(0,0), (1,0), (0,1), (3,5)} 的所有成对差都是本原的，因此其格 Borsuk 数为 4 = 2^2，而其凸包包含 7 个格点，因而不等价于任何正方形。该反驳已形式化验证：一个约 1100 行的 Lean 4 开发（基于 mathlib）证明了 betaZ SA = 4、latticeCount hullSA = 7 和 conjecture3_false；公理审计仅报告三个标准公理。另外两个反例（精确算术，未形式化）在二维和三维中完成了自然的修复。

Elizalde–Luo — papers/elizalde-luo/note.pdf

避免 1132 和 3312 的非嵌套排列的 Elizalde–Luo 猜想证明。 Elizalde 和 Luo（DMTCS 27:1, 2025）根据 n ≤ 8 的数据猜想，同时避免 1132 和 3312 的 {1,1,…,n,n} 的非嵌套排列数为 3^n − 3·2^(n−1) + 1。论文用初等自包含论证（Dyck 形状携带标签排列；避免条件导致前缀区间标签；交叉弧上的双色条件）证明了该猜想，并给出了第二个双射证明（映射到一个显式的三进制语言）。每个引理都在远超原始数据范围的机械验证下完成，包括对 n = 8 时所有 57,657,600 个非嵌套词的穷举检查。完整的通项 n 定理现在已在 Lean 4 中形式化并被 Lean 核心接受（problems/p3-moonshot/elizalde-luo/lean/，定理 elizalde_luo_1132_3312；无 sorry，无 native_decide，公理审计仅报告三个标准 mathlib 公理），因此结果等级为 kernel。

Sun 4.6 — papers/sun-46/note.pdf

Sun 的三角永久行列式的符号模式。 Zhi-Wei Sun（arXiv:2108.07723，猜想 4.6）猜想了由三角矩阵的永久行列式导出的两个整数序列的符号模式。第 (ii) 部分——即整个猜想——在 p = 29 处失败，这是 Sun 发表表格之后的第一个素数：s_29 = 1,053,859 > 0 尽管 29 ≡ 5 (mod 12)，且 s’_29 = −4,806,838,304 < 0 尽管 29 ≡ 5 (mod 8)。每个值都至少由四个独立编写的精确程序中的两个认证（大整数分圆算术；有限域特化结合 CRT 唯一性证明）；该管线重现了 Sun 的所有 19 个已发表值。第 (i) 部分通过了所有测试，仍然开放。

无五点球面记录 — papers/no5sphere-record/note.pdf

13×13×13 网格中的一个 36 点子集。 对于 C(n)，即 {1,…,n}^3 中无五点共球或共面的最大子集，7 ≤ n ≤ 12 时最强的已知下界来自 AlphaEvolve，最终得到 C(12) ≥ 33。论文展示了一个显式的中心对称的 {0,…,12}^3 的 36 点子集，证明了 C(13) ≥ 36。验证是一个有限精确整数计算——所有 376,992 个升序 5×5 行列式均非零——由一份完整打印的 21 行程序重现，并由三个独立编写的检查器执行，这些检查器通过变异测试验证。

Graffiti 143 和 154 — papers/graffiti-143-154/note.pdf

图特征值上两个 Graffiti 猜想的反例。 来自 Fajtlowicz 的 Graffiti 程序的两个谱猜想，均经受住了 Brewster–Dinneen–Faber 1990–91 年的计算攻击和 2025 年八种算法的搜索，现被反驳。猜想 143 在哑铃图上失败（最小认证反例：在两种平均距离约定下均为 39 个顶点），两侧比值趋于 2。猜想 154（标准差解读）在棒棒糖图上于 118/120 个顶点处失败，比值无界。所有反例均附有精确有理数证书，每个结果由两条算法独立的路径验证。

Kurkov A000670 — papers/kurkov-a000670/note.pdf

Kurkov 2018 年关于 Fubini 数猜想的证明。 在 OEIS A000670（Fubini 数，计算 n 元集的有序划分）中，Mikhail Kurkov 于 2018 年 7 月猜想：对于 n > 0，a(n) = Sum_{k=0..2^(n-1)−1} A284005(k)。论文通过一个精细化定理证明：将 k 编码为 (n−1) 位字符串 b 固定一组块最小值 M(b)，且 [n] 上具有该最小值集的有序划分的数量恰好等于乘积 ∏(1 + w_i) = A284005(k)，因此对所有 k 求和即得 a(n)。该精细化结果在 n ≤ 8 时对所有最小值集进行了穷举验证（共 598,444 个有序划分，0 个不匹配），数值上验证至 n = 20，并使用经过变异测试的检查器。

Lean 项目

Borsuk（kernel 等级声明） — problems/p3-moonshot/borsuk/lean/。包含固定的工具链 leanprover/lean4:v4.30.0 和固定的 mathlib 清单；多 GB 的 .lake/ 构建缓存不包含在内。要运行内核检查：

cd problems/p3-moonshot/borsuk/lean
lake update                  # 解析固定依赖；mathlib 的钩子会获取构建缓存
lake build                   # 预期 "Build completed successfully"
lake env lean scripts/CheckAxioms.lean   # 预期仅输出：propext, Classical.choice, Quot.sound

参见 problems/p3-moonshot/borsuk/lean/SETUP.md 获取完整的固定版本表和故障排除。构建完成后，verify_all.py 会自动加载两个 Borsuk 检查（33/33 PASS）。

Elizalde–Luo（第二个 kernel 等级声明） — problems/p3-moonshot/elizalde-luo/lean/。完整的通项 n 定理 elizalde_luo_1132_3312 已形式化并被 Lean 核心接受——无 sorry，无 admit，无 native_decide；公理审计仅报告三个标准 mathlib 公理。构建并重新检查：

cd problems/p3-moonshot/elizalde-luo/lean
lake update                  # 解析固定依赖；mathlib 的钩子会获取构建缓存
lake build                   # 预期 "Build completed successfully"
lake env lean scripts/AxiomCheck.lean   # 预期仅输出：propext, Classical.choice, Quot.sound

参见 problems/p3-moonshot/elizalde-luo/lean/STATUS.md 获取完整的绿灯表格（构建、sorry/公理 grep、#print axioms、n ≤ 4 正确性检查层）。

Erdős #866（kernel 等级头条定理） — problems/p4-erdos866/lean/。精确值定理 Erdos866.h4_eq_4（对所有 n ≥ 331,777 有 h4(n) = 4，两半部分）、4 ≤ h4(n) ≤ 1000、首个严格 g4 < h4 分离（超出 k = 3）、g5 < 3,519,220 以及 h5 的 Fibonacci 下界——全部无 sorry，仅依赖三个标准公理。注意它固定了上游的工具链（leanprover/lean4:v4.28.0，mathlib 8f9d9cff），并提供了 van Doorn 公开形式化的字节完全相同的版本；参见 problems/p4-erdos866/lean/SETUP.md 以及审计脚本 scripts/AuditC4P1.lean / scripts/AuditC4Synth.lean。

并闭集 / Frankl 常数 — problems/p6-moonshot/uc-frankl/lean/。一个经 kernel 检查的归约，证明 franklWithConstant_psi：并闭集常数 ψ = (3 − √5)/2 是一个有效的 Frankl 频率界（每个非空有限并闭族都有一个元素，该元素出现在至少 ψ 比例的子集中）。同样的公理纪律——lake env lean scripts/CheckAxioms.lean 报告每个封闭定理（包括 franklWithConstant_psi）仅使用 propext、Classical.choice、Quot.sound。

布局

• RESULTS.md、VALIDATION.md、verify_all.py — 目录、阅读指南、主程序集
• papers/ — 六篇论文源码 + PDF、构建说明、审稿回复、重新计算脚本
• problems/p0-iris/ — IRIS 6.1 反例：证书、双检查器（Python + Rust）、变异检查套件
• problems/p2-factory/kills/ — 每个被反驳猜想一个目录：冻结声明、证书、检查器、变异检查套件、说明；problems/p2-factory/verify_kills.py 从头重新推导五个“击杀”
• problems/p2-factory/attacks/sun-46/ — Sun 4.6“击杀”的洁净室验证侧（精确子集 DP 层、精确分圆层、CRT 唯一性证明、原始日志）
• problems/p1-records/no-5-on-a-sphere-grid/ — C(13) ≥ 36 证书、三个检查器路径、对抗性跨模型检查器、来源、构造挖掘说明
• problems/p3-moonshot/borsuk/ — Lean 4 项目（kernel 证明）、论文源码、状态
• problems/p3-moonshot/elizalde-luo/ — 固定定义、地面真相枚举器（Python/Rust/洁净室）、审计证明草稿、抽查审计及 kernel 检查的 Lean 4 证明（lean/，定理 elizalde_luo_1132_3312）
• problems/p4-erdos866/ — Erdős #866 版本：冻结论文、完整 Lean 4 开发（Erdos866.h4_eq_4 及其他 kernel 声明）、带 sha256 的冻结验证报告、检查器脚本及 SAT 证书归档清单（4.4 GB 的 DRAT/LRAT 归档本身位于 Zenodo — problems/p4-erdos866/RETRIEVAL.md）

与内部工作树的差异

这是一个精心策划的快照。为保持完全透明，在此列出暂存时所做的每项调整：

1. verify_all.py：两个 Borsuk Lean 检查现在在 .lake/packages 缺失时会给出 SKIP（并附说明），而不是静默启动从零开始的数小时 mathlib 构建。没有其他