M08
用 Walnut 自动定理证明器批量判定 OEIS 自动序列条目的未证猜想：形式化管道与新定理清单
1 · 研究问题
OEIS 中以 k-自动（k-automatic）或 Fibonacci-自动序列描述、且注记含未证陈述（"Conjecture"“It appears"）的条目里，哪些可写成 Walnut 可判定的一阶逻辑语句？批量形式化-判定管道能产出多少条新定理与多少条被证伪的猜想？
2 · 研究背景与空白
Walnut（Mousavi 2016；Shallit 专著 2022）实现了自动序列一阶性质的机械判定：性质写成含加法与序列取值的一阶语句后，程序把它编译为自动机并给出 TRUE/FALSE 及反例。它已在 70+ 篇文献中证明定理甚至纠正错误结论；最显而易见的做法已被做过——Shallit 2025（arXiv:2503.04122）即用 Walnut 解决了一批 OEIS 问题。
空白在该文覆盖的是作者挑选的条目，OEIS 中符合条件的候选远未穷尽，且无人发布"系统抓取 → 形式化 → 判定"的可复用管道与判定率统计。差异轴是换样本 + 方法学产品化：学生贡献一份与 2503.04122 逐条去重的新判定清单和一个开源管道。适合逻辑敏感的学生：单条成功即是一个可署名的机器证明定理。
历届对照：2020 年铜奖《O(1) Algorithm for Calculating Prefix Sum of Fibonacci Words》属自动序列圈内的单序列算法工作；本题是批量机器证明，对象与产出形态不同。
3 · 可检验假设
- H1：候选清单中 ≥ 20% 可形式化为 Walnut 语句，其中 ≥ 50% 在 16 GB 内存内判定成功。
- H2：至少 1 条 OEIS 未证陈述为假（Walnut 给出显式反例下标）。
4 · 量化验收标准
- 方法学校验（硬门槛）：用 Walnut 命令级复现 ≥ 5 个已发表定理（如 Thue–Morse 无重叠因子、Fibonacci 词的平衡性），输出全部为 TRUE 且与文献一致；不吻合（含环境问题）则后续无效。
- 候选清单 ≥ 40 条（抓取脚本 + 人工筛选记录全存档），并与 arXiv:2503.04122 及 Walnut 文献列表逐条去重。
- 新判定 ≥ 8 条；每条给出 Walnut 语句、判定结果、自动机状态数与运行资源。
- 失败案例分类报告：不可形式化（性质非一阶/涉及任意底数）、资源爆炸（状态数曲线）、判定为假（反例验证到 OEIS b-file）。
- 管道（抓取 + 模板 + 命令）开源，第三方可对新条目复用。
5 · 数据与工具
| 用途 | 来源 / 工具 |
|---|---|
| 判定引擎 | Walnut（免费 Java；内置 msd_k / Fibonacci / Tribonacci / Pell 等数系、自动机决策过程与反例输出；不内置：从自然语言到一阶语句的翻译——这是本项目人力核心） |
| 资源边界 | 中间自动机可指数爆炸；16 GB 笔记本可处理中小语句，爆炸实例记为"资源内不可判定"并计入第 4 条报告 |
| 候选抓取 | OEIS JSON API（公开，keyword 与正文检索；b-file 用于反例数值复核） |
| 已有成果对照 | Shallit 2025、Walnut 书——仅校验与去重用，不计入贡献 |
6 · 方法路径
- 装 Walnut，完成 5 个复现校验。
- 写 OEIS 抓取脚本，生成并人工清洗候选清单。
- 建立"猜想类型 → 语句模板"对照表（周期性、出现位置、正则性、部分和同余等）。
- 逐条形式化并判定，记录状态数与资源曲线。
- 对判定为假的条目，用 b-file 独立数值验证反例，并按 OEIS 流程提交更正（署名贡献）。
- 汇总判定率统计与失败分类，形成方法学结论。
7 · 新颖性边界
Walnut 本身、决策过程理论与"用 Walnut 攻 OEIS"的思路均已发表（Mousavi 2016；Shallit 2022 专著；arXiv:2503.04122），本项目不声称工具或思路原创。贡献（主结论）：与已有文献去重后的新判定清单（每条是一个此前未证的定理或被证伪的猜想）+ 首个公开的可复用批量管道与判定率数据。价值：判定清单是硬增量；即便 H2 落空、判定数偏低，判定率与失败分类本身回答了"这类猜想有多少落在机械可判定范围内"这一方法学问题——正负都成文。
8 · 决策门槛（go / no-go）
- 第 4 周末：5 项复现全过（Java 环境与数系文件核实完毕）。
- 第 8 周末：候选清单规模检查。若 < 20 条 → 扩大检索面（加变换类：transduction 可及的序列、negative base 条目）；仍不足则把范围扩到"文献中标注 open 的自动序列问题"清单，管道不变。
- 第 16 周末：若新判定 < 3 条 → 降级：主结论转为"机械可判定性的实证边界研究"（形式化失败与资源爆炸的系统分类 + 状态数增长测量），保留管道框架与全部已得判定。
- 已知风险写死：单条大语句可跑数天，须设 48 h/16 GB 硬截断并记录，不允许无限期挂机。