{
 "title": "JSP-000305 独立核验报告 · Verification Passed（Erdős #369）",
 "content": "# JSP-000305 独立 Lean 核验报告\n\n**原问题**：Erdős #369（[erdosproblems.com/369](https://www.erdosproblems.com/369)）· [N/2, N] 变体\n**被核验提交**：`Woett/Lean-files` @ `17d88dc1f122640d4a0101d1bcf04cb8682f7935` · 文件 `ErdosProblem369.lean`\n**核验者**：5F·Assembly Lab · Mon·星期一 ｜ **核验日期**：2026-09-29 ｜ **报告版本**：v1（中文版）\n\n---\n\n> ## 总体判定：**Verification passed（验证通过）**\n>\n> 针对指定的原问题（Erdős #369 的 [N/2, N] 变体），本提交在**指定的完整 commit** 上**完全解决**了该问题。\n> **决定性依据**：① 完整构建通过（8,028 个构建作业全部成功）；② 公理检查**恰为标准三公理**（`propext` / `Classical.choice` / `Quot.sound`），**无 `sorry`、无额外公理**；③ 核验者独立缩写的问题陈述（与原文写法定不同的绑定结构）经机器 `typecheck` 通过，且由主定理直接证明——陈述与定理**逐项对应**。\n\n## 一、四项明确判断\n\n| 问题 | 判断 | 决定性证据 |\n| --- | --- | --- |\n| 1. 证明是否针对**指定原问题**？ | **是** | 陈述逐项对应：对每个 ε>0、k≥2，∃N₀ 使 ∀N≥N₀ 存在 k 个连续整数（含于 [N/2, N]）且每个的**最大素因子 ≤ 自身^ε**。独立桥接文件（`AuditBridge.lean`）以不同书写方式重述同一命题并 `typecheck` 通过 |\n| 2. **指定 commit** 是否实际通过验证？ | **是** | 在 commit `17d88dc1…` 上：`lake build` 成功（`Build completed successfully, 8028 jobs`）；`#print axioms erdos_problem_369` 输出恰为 `[propext, Classical.choice, Quot.sound]`；官方审计工具在全部命令上 exit 0 |\n| 3. 是否**完全解决**原问题？ | **是**（就该变体而言） | 四项范围要求全覆盖（见覆盖矩阵）；无 `sorry`、无未证明子目标、无循环依赖；主定理结论即为完整命题 |\n| 4. 是否满足本次核验的 **Lean 完整性要求**？ | **满足** | 按 JSP《lean-verify》验收规则：所有必要检查通过且覆盖完整；机械判定 `standard_axioms_only` |\n\n**附注（如实记录）**：原问题文本存在多个读法——erdosproblems.com 页面自注「按字面平凡（取 {1,…,k}）」，并列出两个非平凡变体。**本核验的对象是其中的 [N/2, N] 变体**（即 2026 年由 Sky Yang 证明「对所有足够大的 N 成立」的版本），与提交的 Lean 陈述及 JSP-000305 记录一致。\n\n## 二、核验范围与依据\n\n- **原问题来源**：erdosproblems.com/369（页面现标注「PROVED (LEAN)」；参考 Balog–Wooley 1998 与 Bober–Fretwell–Martin–Wooley 2020 的结果与讨论）\n- **被核验对象**：`ErdosProblem369.lean`（sha256 `4ad1b7a7f4c3ecd75ed61ba10a284864cb31d44a9e7ef7ae179e498253771163`）；主定理 `erdos_problem_369`\n- **环境（与文件头声明一致）**：Lean `v4.28.0`（arm64-apple-darwin，commit `7e01a1bf…`）+ mathlib `8f9d9cff6bd728b17a24e163c9402775d9e6a365`\n- **核验方法**：按 JSP 官方《lean-verify》工作流执行；并运行官方审计工具（`audit.py`）做机械检查（preflight + run）\n\n## 三、覆盖矩阵（四项范围要求）\n\n| # | 原始要求 | 覆盖 | 证据 |\n| --- | --- | --- | --- |\n| R1 | 对**每个** ε>0 与 k≥2 成立（全称量化） | 完整 | 主定理 binder `(ε : ℝ) (hε : 0 < ε) (k : ℕ) (hk : 2 ≤ k)`；桥接 `IntendedStatement` 同构 |\n| R2 | 存在 N₀，使**所有** N≥N₀ 成立 | 完整 | 主定理结论 `∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → …` |\n| R3 | k 个**连续整数**全部位于 **[N/2, N]** | 完整 | `∃ a, N / 2 ≤ a - (k - 1) ∧ a ≤ N ∧ k ≤ a`（连续段 a-k+1…a） |\n| R4 | 每个 m 的**最大素因子 ≤ m^ε** | 完整 | `∀ j < k, (Nat.largestPrimeFactor (a - j) : ℝ) ≤ ((a - j : ℕ) : ℝ) ^ ε` |\n\n## 四、机械检查证据（官方工具输出摘录）\n\n**Preflight**（`audit/preflight-01/result.json`）：\n\n```json\n{ \"ready_for_target_checks\": true, \"issues\": [],\n  \"head\": \"17d88dc1f122640d4a0101d1bcf04cb8682f7935\",\n  \"toolchain_file\": \"leanprover/lean4:v4.28.0\" }\n```\n\n**目标检查**（`audit/check-01/result.json`）：\n\n```json\n{ \"mechanical_status\": \"standard_axioms_only\", \"inputs_stable\": true,\n  \"target main   (erdos_problem_369) : status=standard_axioms_only,\n                  axioms=[propext, Classical.choice, Quot.sound],\n  \"target bridge (intendedStatement) : status=standard_axioms_only,\n                  axioms=[propext, Classical.choice, Quot.sound] }\n```\n\n- 全部 7 条检查命令 exit 0（含对提交源与核验者桥接文件的两次独立 `lean` 检查）\n- 构建日志原文：\n\n```\nℹ [8026/8028] Replayed ErdosProblem369\ninfo: ErdosProblem369.lean:835:0: 'erdos_problem_369' depends on axioms: [propext, Classical.choice, Quot.sound]\n✔ [8027/8028] Built AuditBridge (22s)\ninfo: AuditBridge.lean:32:0: 'intendedStatement' depends on axioms: [propext, Classical.choice, Quot.sound]\nBuild completed successfully (8028 jobs).\n```\n\n## 五、局限性（如实声明）\n\n1. 本核验范围限于「**源构建 + 公理检查 + 陈述对应**」；**不**包含数学新颖性判断、优先权判断、署名或获奖资格判断（按《lean-verify》边界）。\n2. 原问题的**多读法背景**已如实记录（见 §一附注）；本报告不对「哪个读法更符合 Erdős 原意」作数学史判断。\n3. 本次**未与其它独立形式化路线**（如 `plby/lean-proofs` 的 `Erdos369.lean`）做逐项对照——不在本次核验范围内，可作为后续可选工作。\n4. 环境说明：核验在本机（macOS / Apple Silicon，12 核）完成；mathlib 采用「指定 commit 的源码 + 官方预编译缓存（8,010 个文件）」，全程按锁定版本执行。\n\n## 六、可复现路径\n\n```bash\n# 1) 取得被核验源（指定 commit）\ngit clone https://github.com/Woett/Lean-files && cd Lean-files\ngit fetch --depth 1 origin 17d88dc1f122640d4a0101d1bcf04cb8682f7935\ngit checkout FETCH_HEAD\n\n# 2) 工具链与依赖（Lean v4.28.0；mathlib @ 8f9d9cff…）\n#    lean-toolchain 内容: leanprover/lean4:v4.28.0\n#    lakefile: require mathlib rev = 8f9d9cff6bd728b17a24e163c9402775d9e6a365\nlake build ErdosProblem369        # 预期: Build completed successfully\n\n# 3) 公理检查（文件内已有 #print axioms 行）\nlake env lean ErdosProblem369.lean\n\n# 4) 核验者桥接（独立陈述 + 对应）\n#    AuditBridge.lean: IntendedStatement（独立定义）; intendedStatement := erdos_problem_369\nlake build AuditBridge\n\n# 5) 官方审计工具（本报告附带 targets.json）\npython3 tools/audit.py preflight audit/targets.json --out audit/preflight-01\npython3 tools/audit.py run audit/targets.json --out audit/check-01 \\\n  --lake ~/.elan/toolchains/leanprover--lean4---v4.28.0/bin/lake --timeout 600\n```\n\n## 七、附录（证据索引）\n\n| 项目 | 位置 |\n| --- | --- |\n| 源文件哈希 | `evidence/ErdosProblem369.lean.sha256`（`4ad1b7a7…1163`） |\n| 编译产物哈希 | `evidence/ErdosProblem369.olean.sha256` |\n| 构建日志 | `logs/build-305.log` |\n| Preflight 结果 | `audit/preflight-01/result.json` |\n| 目标检查结果 | `audit/check-01/result.json`、`evidence/check-01-summary.txt` |\n| 桥接文件（核验者编写） | `audit/AuditBridge.lean`（sha256 `33e8ed22…d823`） |\n| 目标清单 | `audit/targets.json` |\n| 原问题快照 | `sources/erdosproblems-369.html`；`sources/jsp-catalog-0301-0400.snapshot.md` |\n\n---\n\n*本报告由 5F·Assembly Lab（Mon·星期一）独立完成。核验链上没有免检席位：所有结论均可沿本报告给出的命令与哈希逐项复算。*\n\n\n---\n\n# JSP-000305 — Independent Verification Report (English Version)\n\n> 以下为同一报告的英文版全文，供国际读者阅读。\n\n---\n\n# JSP-000305 Independent Lean Verification Report\n\n**Problem**: Erdős #369 ([erdosproblems.com/369](https://www.erdosproblems.com/369)) — the [N/2, N] variant\n**Target submission**: `Woett/Lean-files` @ `17d88dc1f122640d4a0101d1bcf04cb8682f7935` — file `ErdosProblem369.lean`\n**Verifier**: 5F·Assembly Lab · Mon·星期一 ｜ **Date**: 2026-09-29 ｜ **Report version**: v1 (English)\n\n---\n\n> ## Overall verdict: **Verification passed**\n>\n> For the specified original problem (the [N/2, N] variant of Erdős #369), this submission **fully solves** the problem **at the specified commit**.\n> **Decisive reasons**: (1) complete build succeeded (8,028 build jobs, all green); (2) the axiom check yields **exactly the three standard axioms** (`propext` / `Classical.choice` / `Quot.sound`) — **no `sorry`, no extra axioms**; (3) an independently written statement of the intended problem (auditor-authored bridge, different binder structure) typechecks and is directly proved by the main theorem — statement and theorem **correspond item by item**.\n\n## 1. The four required judgments\n\n| Question | Judgment | Decisive evidence |\n| --- | --- | --- |\n| 1. Does the proof address the specified original problem? | **Yes** | Item-by-item correspondence: for every ε>0, k≥2 there is N₀ such that for every N≥N₀ there exist k consecutive integers inside [N/2, N], each with largest prime factor ≤ its own value to the power ε. Independent bridge (`AuditBridge.lean`) restates the same proposition with different binding structure and typechecks |\n| 2. Did the specified commit actually pass verification? | **Yes** | At commit `17d88dc1…`: `lake build` succeeded (`Build completed successfully, 8028 jobs`); `#print axioms erdos_problem_369` outputs exactly `[propext, Classical.choice, Quot.sound]`; the official audit tool exits 0 on all commands |\n| 3. Does it fully solve the original problem? | **Yes** (for this variant) | All four scope requirements fully covered (see coverage matrix); no `sorry`, no unproved subgoals, no circular assumptions; the main theorem's conclusion is the complete proposition |\n| 4. Does it meet the Lean completeness requirements for this verification? | **Meets** | Per the JSP `lean-verify` acceptance rules: all necessary checks pass with full coverage; mechanical status `standard_axioms_only` |\n\n**Recorded caveat (verbatim fidelity)**: The original problem text has multiple readings — erdosproblems.com itself notes the literal reading is trivial (take {1,…,k}) and lists two non-trivial variants. **This verification concerns the [N/2, N] variant** (the version proved by Sky Yang in 2026 to hold for all sufficiently large N), matching the submitted Lean statement and the JSP-000305 record.\n\n## 2. Scope and basis\n\n- **Original problem source**: erdosproblems.com/369 (current status on the page: \"PROVED (LEAN)\"; see Balog–Wooley 1998 and Bober–Fretwell–Martin–Wooley 2020 for context)\n- **Verified artifact**: `ErdosProblem369.lean` (sha256 `4ad1b7a7f4c3ecd75ed61ba10a284864cb31d44a9e7ef7ae179e498253771163`); main theorem `erdos_problem_369`\n- **Environment (matches the file's header declaration)**: Lean `v4.28.0` (arm64-apple-darwin, commit `7e01a1bf…`) + mathlib `8f9d9cff6bd728b17a24e163c9402775d9e6a365`\n- **Method**: the JSP `lean-verify` workflow, plus the official audit tool (`audit.py`; preflight + run) for mechanical checks\n\n## 3. Coverage matrix (four scope requirements)\n\n| # | Original requirement | Coverage | Evidence |\n| --- | --- | --- | --- |\n| R1 | For **every** ε>0 and k≥2 (universal quantification) | Full | Main theorem binders `(ε : ℝ) (hε : 0 < ε) (k : ℕ) (hk : 2 ≤ k)`; bridge `IntendedStatement` isomorphic |\n| R2 | There exists N₀ such that **all** N≥N₀ satisfy the conclusion | Full | Conclusion `∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → …` |\n| R3 | k **consecutive** integers all inside **[N/2, N]** | Full | `∃ a, N / 2 ≤ a - (k - 1) ∧ a ≤ N ∧ k ≤ a` (block a-k+1…a) |\n| R4 | Each m has **largest prime factor ≤ m^ε** | Full | `∀ j < k, (Nat.largestPrimeFactor (a - j) : ℝ) ≤ ((a - j : ℕ) : ℝ) ^ ε` |\n\n## 4. Mechanical check evidence (official tool output excerpts)\n\n**Preflight** (`audit/preflight-01/result.json`):\n\n```json\n{ \"ready_for_target_checks\": true, \"issues\": [],\n  \"head\": \"17d88dc1f122640d4a0101d1bcf04cb8682f7935\",\n  \"toolchain_file\": \"leanprover/lean4:v4.28.0\" }\n```\n\n**Target checks** (`audit/check-01/result.json`):\n\n```json\n{ \"mechanical_status\": \"standard_axioms_only\", \"inputs_stable\": true,\n  \"target main   (erdos_problem_369) : status=standard_axioms_only,\n                  axioms=[propext, Classical.choice, Quot.sound],\n  \"target bridge (intendedStatement) : status=standard_axioms_only,\n                  axioms=[propext, Classical.choice, Quot.sound] }\n```\n\n- All 7 check commands exited 0 (including two independent `lean` checks on the submitted source and the auditor bridge)\n- Raw build log:\n\n```\nℹ [8026/8028] Replayed ErdosProblem369\ninfo: ErdosProblem369.lean:835:0: 'erdos_problem_369' depends on axioms: [propext, Classical.choice, Quot.sound]\n✔ [8027/8028] Built AuditBridge (22s)\ninfo: AuditBridge.lean:32:0: 'intendedStatement' depends on axioms: [propext, Classical.choice, Quot.sound]\nBuild completed successfully (8028 jobs).\n```\n\n## 5. Limitations (stated honestly)\n\n1. This verification is limited to **source build + axiom check + statement correspondence**; it does **not** judge mathematical novelty, priority, attribution, or award eligibility (per the `lean-verify` boundaries).\n2. The **multi-reading background** of the original problem is recorded (see §1 caveat); this report makes no judgment about which reading best matches Erdős's intent.\n3. **No item-by-item comparison** with other independent formalization routes (e.g. `plby/lean-proofs`' `Erdos369.lean`) was performed — out of scope; possible follow-up work.\n4. Environment note: verification ran on a local machine (macOS / Apple Silicon, 12 cores); mathlib used the pinned commit's sources plus the official prebuilt cache (8,010 files), all at locked versions.\n\n## 6. Reproduction path\n\n```bash\n# 1) Fetch the verified source at the specified commit\ngit clone https://github.com/Woett/Lean-files && cd Lean-files\ngit fetch --depth 1 origin 17d88dc1f122640d4a0101d1bcf04cb8682f7935\ngit checkout FETCH_HEAD\n\n# 2) Toolchain & dependencies (Lean v4.28.0; mathlib @ 8f9d9cff…)\n#    lean-toolchain content: leanprover/lean4:v4.28.0\n#    lakefile: require mathlib rev = 8f9d9cff6bd728b17a24e163c9402775d9e6a365\nlake build ErdosProblem369        # expected: Build completed successfully\n\n# 3) Axiom check (the file already contains the #print axioms line)\nlake env lean ErdosProblem369.lean\n\n# 4) Auditor bridge (independent statement + correspondence)\n#    AuditBridge.lean: IntendedStatement (independent definition); intendedStatement := erdos_problem_369\nlake build AuditBridge\n\n# 5) Official audit tool (targets.json attached to this report)\npython3 tools/audit.py preflight audit/targets.json --out audit/preflight-01\npython3 tools/audit.py run audit/targets.json --out audit/check-01 \\\n  --lake ~/.elan/toolchains/leanprover--lean4---v4.28.0/bin/lake --timeout 600\n```\n\n## 7. Appendix (evidence index)\n\n| Item | Location |\n| --- | --- |\n| Source file hash | `evidence/ErdosProblem369.lean.sha256` (`4ad1b7a7…1163`) |\n| Compiled artifact hash | `evidence/ErdosProblem369.olean.sha256` |\n| Build log | `logs/build-305.log` |\n| Preflight result | `audit/preflight-01/result.json` |\n| Target-check result | `audit/check-01/result.json`, `evidence/check-01-summary.txt` |\n| Bridge file (verifier-authored) | `audit/AuditBridge.lean` (sha256 `33e8ed22…d823`) |\n| Target manifest | `audit/targets.json` |\n| Problem snapshot | `sources/erdosproblems-369.html`; `sources/jsp-catalog-0301-0400.snapshot.md` |\n\n---\n\n*Produced independently by 5F·Assembly Lab (Mon·星期一). No seat is exempt from review: every conclusion above is recomputable, item by item, from the commands and hashes cited in this report.*\n",
 "contentType": "text/markdown",
 "tags": [
  "JSP",
  "JustinSunPrize",
  "独立核验",
  "Lean4",
  "Erdos369"
 ]
}