CrocSwap/integer-mult-bounds · 上手攻略

• 仓库：CrocSwap/integer-mult-bounds
• 链接：https://github.com/CrocSwap/integer-mult-bounds
• 分类：engineering / formal verification / integer arithmetic
• 作者：spark
• 更新：2026-10-14

§0 三证 checklist - GitHub URL：✅ 已 fetch（README + certificates/selected-result.json + docs/research/*） - 顶会 venue+年份：⚠️ 该项目为社区协作形式化研究，未绑定顶会 anchor；README 与 PR 描述均称结果"conditional on the OpenAI #109 framework"。本文不引入未经核实的会议背书。 - README 子模块 anchor：✅ autoresearch.md（任务选择与协调）+ AGENTS.md + CONTRIBUTING.md + docs/research/bottleneck-brief.md + certificates/selected-result.json

一、是什么

CrocSwap/integer-mult-bounds 是一个社区维护的 Python 研究仓库，目标是"在 OpenAI #109 框架之上，为条件整数乘法寻找尽可能大的 κ（kappa），使 T(n) = O!(n (log n)^{1-κ})"。仓库当前 selected κ 为 836330098538459 / 500000000000000000 ≈ 0.001673（README 引自 PR #1094 / 43-contribution review 1099 系列）。

它不是一个面向终端用户的"产品"，而是一个研究审计 + 形式化候选 + 社区接力的工作台：

• README 列出的 construction evidence 是逐步累加的（每条 PR 配一份 review + checkpoint + JSON 证书）；
• 每个候选结果都对应 make frontierXXX-verify / make gen4-bank-verify / make entrance-bank-verify / make recycled-bit-verify 这类 Makefile 目标；
• 主线 PR 列表从 #1094（Kothe–Arun alt-packing，2026 顶部 κ）一路向下到 #135/#144/#186/#210/#276+#279/#531/#535/#588/#617/#626/#1094 系列。

⚠️ 工程边界声明（来自 README 与 REVIEW 文档原文）：仓库多次强调"All-size/compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, exact recovery and analytic obligations remain conditional. This is not a complete Lean multiplication theorem."——即 README 自陈当前不是完整的 Lean 形式化定理，本文不引申为可投产形式化证明。

二、解决什么问题

1. 整数乘法复杂度界探索：试图以"条件构造 + 精确证书 + 可复现审计"的方式逼近更紧的 n (log n)^{1-κ} 上界，并把 κ 的数值、构造来源、证书哈希全部存到 JSON 里，供后续独立核验。
2. 社区协作的 attribution 与 certificate 体系：每条 PR 都配一份 docs/research/community-*-review.md + certificates/checkpoints/*.json，让 audit 链可回溯，避免"在 AI 自动生成 PR 噪声中丢失贡献记录"。
3. AI 代理/作者捐赠算力/写 PR 的接入规范：autoresearch.md / AGENTS.md / CONTRIBUTING.md 明确写了"想贡献 inference 的代理"应该怎么选任务、如何避免重复、如何在 discussion board 登记认领。

三、快速安装

⚠️ 项目自陈 requires C++17 compiler and Boost headers（README），不是纯 Python 工具链；下面是 README 自带的 Python 依赖侧。

# 克隆
git clone https://github.com/CrocSwap/integer-mult-bounds
cd integer-mult-bounds

# Python 侧依赖（README 直接给出的两套 requirements，对应两个研究子目录）
python3 -m pip install numpy sympy scipy
# 若要复现 gen4 / 1099 顶部 κ：
python3 -m pip install -r research/five-stage-gen4-banks/requirements.txt
make frontier1094-verify
make gen4-bank-verify

# 复现较早的 gen4 之前结果：
python3 -m pip install -r research/five-stage-source527-banks/requirements.txt
make source527-verify

# 复现更早的 entrance-bank / recycled-bit 阶段：
make entrance-bank-verify
make recycled-bit-verify

⚠️ 上面的 Makefile target 名来自 README 与 docs/research/community-batch1099-review.md 的实际措辞；C++17 + Boost 这条编译侧依赖不在 Python requirements 列表里，实际复现前应阅读对应子目录的 PROOF.md 与 certificate.json 以确认完整构建链。

四、核心用法（给可复制命令或代码）

仓库的"核心用法"不是调用一个 API，而是跑一个或多个 Makefile target，让对应 witness κ 与"完整 47 个 assembly inequalities + 8 阶段 finite check"重跑一次。下面是从 README 中 verbatim 抽出的几条 entry：

# 1) 跑当前顶部 κ（PR #1094）的验证链路
make frontier1094-verify

# 2) 跑 gen4 banks（PR #276+#279 组合，κ ≈ 0.0007236）
make gen4-bank-verify

# 3) 跑 entrance-bank 阶段（PR #186，Dugongue）
make entrance-bank-verify

# 4) 跑 recycled-bit 阶段（PR #144/#147/#148/#150/#146，icekylinx）
make recycled-bit-verify

每条 make target 都对应一份：

• docs/research/community-*-review.md（人类写的 review，标注哪些条 PR 进入了 selected κ、哪些只是 retained for credit）；
• certificates/checkpoints/*.json（精确证书，记录 κ 数值、有几个 stage pass、47 个 inequality 是否全部满足）；
• research/<topic>/PROOF.md + certificate.json（构造论证与本目录审计快照）。

作为代理贡献者的入口

autoresearch.md + AGENTS.md 给"AI 代理/外部贡献者"列出的标准流程是：

1. 读 docs/research/bottleneck-brief.md，看当前瓶颈；
2. 读 AGENTS.md + CONTRIBUTING.md，看提交规范与许可证（仓库卡片显示 Apache-2.0）；
3. 在 discussion 1163（coordination guide）下登记认领，避免与他人 PR 重复；
4. 在 PR 描述里引用具体的 review/checkpoint 文件路径，让 audit 链可追；
5. 把"未进入 selected κ 但被 retained for credit"的工作单独写在 discussion 上，保持 attribution 干净。

五、典型适用场景

• 学术/审计读者：想验证 README 自陈的 κ 是否真的一次跑就能复现（README 邀请第三方跑 make frontier1094-verify 与 make gen4-bank-verify，并比对 certificates/selected-result.json）；
• AI 代理/研究自动化作者：想找一个"有 AGENTS.md / CONTRIBUTING.md / autoresearch.md 模板"的社区协作仓库作为范本；
• 形式化 + 数值双轨审计研究者：对"JSON 证书 + 47 个 inequality"作为非 Lean 形式化替代方案的可行性感兴趣；
• 贡献 attribution 体系研究者：关心如何在 AI 协作 PR 洪流中保住"独立贡献者"的归属记录。

六、坑与注意

1. 不是 Lean 形式化定理：README 与各 REVIEW 反复声明 "not a complete Lean multiplication theorem"，不要把它当 mathlib 级别证明来引用。
2. "conditional on OpenAI #109"：README 顶部明示所有结果依赖某个外部 framework；没有该 framework 的本地复现是无效的。
3. κ 是"指数节省"不是"实测加速"：README 多处写 "exponent savings, not practical runtime"——不要把 κ ≈ 0.0017 解释成"乘法快 0.17%"。
4. C++17 + Boost 是隐含依赖：Python 端 requirements.txt 不含，要在子目录 PROOF.md 里逐条确认。
5. PR #1048 仍 open：README 明示 "exact counterexample and certification corrections documented in the review"，不要假设所有 history 都已经闭合。
6. discussion 1200 是工作流反馈入口：仓库维护方主动邀请"workflow feedback"，意味着协调规则还在迭代中。
7. retained-credit vs selected-exponent 是两套账：很多 PR 写了"独立贡献"但没推动 selected κ 上行；引用时需先看对应 review 里是否标了 selected 还是 retained for credit。
8. 自 hosted Linux CI 与主验证流程分离：README 末段明示 "Hosted Linux CI is separate"，本地跑通的链路和 CI 上的可能不是同一份。

七、与同类对比

⚠️ 同行表格只是给读者一个"它在哪个谱系"的粗略坐标，不构成对 Harvey–van der Hoeven 等论文级工作的精确归类。

八、一句话推荐结论

面向研究者 / 形式化审计读者 / AI 协作代理：值得读 README 与 autoresearch.md 一遍，把 make frontier1094-verify 跑一次作为入门体检；面向把整数乘法当业务库使用的开发者：本文不作推荐——这不是一个可被 import 的 library，而是 conditional 形式化候选的研究工作台。