[jackson-shit]

Submission type

Lean proof / formalization only（数学解已有：Golomb 1970，见下）。

Problem

• Problem ID：JSP-000301
• Original problem source：problems/catalog-0301-0400.md#JSP-000301 —— "If two consecutive positive integers are powerful, must at least one be a perfect square?"
• Current entry and proposed change：当前条目为 Current status: Solved（Golomb 反例）、Lean proof: No、Eligible to claim: No。本 PR 仅把 Lean proof 信息更新为 Yes，并附 pinned 外部证明仓库引用；不改动数学状态与归属。
• Related issue：无（不以 issue 投稿）。
• Related PRs and how this contribution differs：同题已有多个未合并的 Lean PR（如 [JSP-000301] Add Lean formalization #5136、JSP-000301: record Lean formalization (scks1/jsp-000301-formalization) #5134、JSP-000301: Lean formalization of the powerful-consecutive-integers disproof #5132、JSP-000301: record Lean formalization #5117，截至 2026-10-26 统计共 41 个开放中同题 PR；2026-10-27 复核时目录仍为 Lean: No、candidates/ 仍无 JSP-000301 条目，即尚无被接受的证明）。本贡献是独立重写的形式化：自有仓库、自有 pinned commit、最小导入构建、附公理审计；不是任何他人证明的复制或镜像。

Formal statement

• Complete mathematical solution：Solomon W. Golomb 1970 年反例 [Go70] Powerful numbers, Amer. Math. Monthly 77(8) (1970), 848–852（DOI: 10.2307/2317020），已记录在目录条目中；反例为 12167 = 23³ 与 12168 = 2³ × 3² × 13²。
• Mathematical review reference：目录条目本身（Solved，Golomb 归属）。
• Formal statement location, pinned to a full commit SHA：https://github.com/jackson-shit/justin-sun-prize-lean/blob/50579a6ecc7ef19a41e5e55ed1e577bf97eab82d/JspLean/Jsp000301.lean
• Fully qualified target theorem name：jsp000301
• Statement origin：按目录原题写出的形式化陈述（需维护者复核）。
• Correspondence to the original problem：定理为 ¬ ∀ m: ℕ, m ≠ 0 → Powerful m → Powerful (m + 1) → IsSquare m ∨ IsSquare (m + 1)，其中 Powerful n:= ∀ p, p.Prime → p ∣ n → p ^ 2 ∣ n（Mathlib 无此数论定义，故自定）；即：并非所有非零 powerful 数的后继都与它构成"其一为平方"的配对。作用域仅 yes/no 问句本身，不含 Erdős [Recipient] JSP-000178: Lean formalization, Erdős 184, the K_{3,n−3} lower bound for decompositions into cycles and edges #365 的计数问题，也不涉及三个连续 powerful 数。

Proof submission

[
{
"repository": "https://github.com/jackson-shit/justin-sun-prize-lean",
"branch": "main",
"commit": "50579a6ecc7ef19a41e5e55ed1e577bf97eab82d"
}
]

• Proof file at the selected commit and fully qualified theorem name：JspLean/Jsp000301.lean，定理 jsp000301。
• How the proof establishes the formal statement：对 m = 12167 应用假设得 IsSquare 12167 ∨ IsSquare 12168；引理证明 12167（唯一素因子 23，23² ∣ 23³）与 12168（素因子仅 2、3、13，平方皆整除）均为 powerful；又两者都在 110² 与 111² 之间故皆非平方，矛盾。证明不含 sorry/admit。

Reproduction

• Exact Lean version and lean-toolchain path：leanprover/lean4:v4.35.0，见仓库根目录 lean-toolchain。
• Pinned dependencies and manifest path：Mathlib v4.35.0，见 lakefile.toml（[[require]] name = "mathlib", rev = "v4.35.0"）与 lake-manifest.json。
• Build instructions pinned to the selected commit：
• git clone https://github.com/jackson-shit/justin-sun-prize-lean && cd justin-sun-prize-lean && git checkout 50579a6ecc7ef19a41e5e55ed1e577bf97eab82d
• lake exe cache get（如可用预编译 Mathlib 缓存）或直接 lake build
• 注意：本证明仅导入三个 Mathlib 模块（Mathlib.Algebra.Group.Even、Mathlib.Data.Nat.Prime.Basic、Mathlib.Tactic.NormNum），未用全量 import Mathlib；证明内容不受导入方式影响，构建在拿到 Mathlib oleans 后很快完成。
• Axiom audit command and output：对定理运行 #print axioms jsp000301，输出为 [propext, Classical.choice, Quot.sound]（仅标准公理）。

Pre-submission Lean verification

• Method：本地 lake build（Lean v4.35.0 + Mathlib v4.35.0 预编译缓存）。
• Checked repository and full commit SHA：与提交版本一致（50579a6ecc7ef19a41e5e55ed1e577bf97eab82d），无差异。
• Verification date and conclusion：2026-10-27 晚，构建成功（843 jobs），公理仅标准三条，无 sorry。
• Limitations：本地构建环境与复核者环境可能不同；建议复核者按上文复现步骤独立重建。

Attribution

• Mathematical solver：Solomon W. Golomb（1970 年反例，[Go70]）。
• Lean formalization author：提交账号本人（jackson-shit）；形式化由账号持有者委托、在其名下仓库中完成并提交。口径说明：Henry 按稿批准开 PR 时未另指定署名，故按"提交账号"这一事实口径填写，不虚构真实姓名；如他想改署名，PR 正文开出后仍可编辑修改。
• Independent verifier：无。
• Public authorship evidence：提交仓库归提交账号本人所有，pinned commit 在该账号名下分支 main 内。

Submission checklist

• 仅改动相关目录条目的 Lean proof 信息，并附证据：是。
• 提交结果完整解决原问题；Lean 证明在指定 commit 完整，无 sorry/admit 或未证假设：是。
• 已链接先前提供的完整数学解与证据，并区分数学解作者与形式化作者：是。
• 认领的是本人原创贡献，commit 在所列分支内，已提供陈述对应、复现命令与公理审计：是。
• 本 PR 不含 Lean 源码、压缩包、二进制、vendored 依赖与私人身份/联系/付款信息：是。