bibkey: oeis2026triage0909
authors: OEIS Foundation Inc.; Codex triage workers
year: 2026
title: 93 OEIS candidates — statement and proof triage, 2026-09-09
doi: null
url: https://oeis.org/
claim: Source-based dispatch screening; no new mathematical theorem or Lean module is claimed.
strata_touched: []
license: citation-only
triage: anchor

93 条 OEIS 候选的批量判形与文献分诊

源码基线固定为 4546f231b3d416239a21d9494974ca3ccf684c7a；Mathlib 钉版为 db584cd6d46c92f209a44c0f1c829460d327499d。本文件是文献与派席建议，不是数学证明、模块准入或冻结记录。产地：一席 Codex 主席、三个同模型族 codex-cli 文献分工席；主席复核候选与关键淘汰依据。使用 lean4 skill 的声明检索部分，未执行 Lean；没有异模型独立共识。

判据与排序

precise 表示定义和量词可明确编码，不表示容易证明；vague 表示原表述或序列成员资格尚依赖未固定语义。档位 1 是可考虑短组合/算术探针，2 是非普通有限实例的计算前沿，3 是需要研究方向的核心/深层目标；out 表示已知、错误、纯定义或本席排除的无界解析目标。即使离散全称陈述 precise，也可能属于 3。

published 只用于公开证明、完整论证或能明确推出目标的已知公式；它包括注明的公开反驳，不等同于“猜想为真”。open 只表示所查材料仍猜想且未找到证明；unknown 表示相关论证、公式证明或定义桥未核实。出现过同一句猜想不算证明。数值 yes 只表示几十行程序可核查有意义的小参数前缀，绝不表示全称可由有限实验确证；no 的条目另解释障碍。

dispatch 按拟议逃逸的明确程度、数值可验性和 open 证据排序；它是有停止条件的后续探针建议，不是已经构造出逃逸见证。同族依赖任务合并派，避免按 A 号重复实施。特别是 A397345（q=5）、A397348（q=3）、A397242（q=1）的奇偶问题只派一个奇数参数卷积任务；A397346（q=2）可共享整数化基础，但模8结论须独立证明。所有签名均为未编译的数学伪签名。bind 风险是源代码声明检索判断：列出的通用声明只说明最接近的候选；none 不是全库不存在定理的证明。

已分诊 93/93 条：dispatch 8，note-only 66，drop 19；文献 open 52，published 11，unknown 30。 93 个输入 A 号均有且仅有一行和一段。

Verified locator

源站 https://oeis.org/ 。2026-09-09 对每个输入以及其 comment / formula / xref 中的全部直接 A 号逐个请求 https://oeis.org/search?q=id:<A号>&fmt=json，保存完整原始 JSON，未截断字段。93 个源条目加 323 个额外引用共 416 个唯一条目，416/416 HTTP 成功、JSON 编号匹配；不是递归遍历所有引用的引用。每段末列出该源条目提取出的完整集合（包括源文自引）；空集合写 none。逐条结论区分“取到完整条目”和“已读链接中的证明”，未打开的链接不当证明。

关键实际打开定位：

• Shah–Kiselev, https://arxiv.org/html/2605.11137v1 ，§3、Claim 4.1、Remark 4：带权和结果与无权奇偶差猜想分开。
• Höft, Theorems Relating to Conjectures by Omar E. Pol (2026-03-21), https://oeis.org/A237270/a237270_4.pdf ，Theorems 1、3、4 及其证明；几何定义桥另逐条判断。
• A395171 公开反驳 https://mathoverflow.net/a/511088 ；存在性论证 https://mathoverflow.net/a/511242 ，已通过 StackExchange API 获取完整回答正文。

原始检索工件在本次 runner attempt 的 oeis/、oeis-manifest.json、refs.json 和分工日志；manifest 含 URL、时间、revision、字节数和 SHA-256。它们是本次机器上的审计工件，未作为仓库附件发布，临时目录不承诺长期可用。本文件中的公开 URL 和具名证明位置是持久查证入口。仓库交付保持单文件。

排序表

逐条依据与实施边界

A387319 — precise；dispatch。 精确目标：def Coincides(k:ℕ):Prop := ∃m:ℕ,6≤m ∧ m≤k ∧ 3∣m ∧ 3*((2k)%m)=m((2k)%3); theorem classify(k:ℕ):Coincides k ↔ 1<k ∧ ¬Nat.Prime k ∧ k∉({4,8,10,25}:Finset ℕ)。交叉乘积等价于原正分母分数相等。 逃逸：新中间命题：写m=3t，重合当且仅当2≤t、3t≤k、t∣2k且((2k/t)%3)=(2k)%3；当3∤k时末项等价于t%3=1。构造：3∣k且k≥6取t=2；偶k且3∤k、k≥12取t=4；奇合数k=pq、p为最小素因子且3∤k，若p%3=1取t=p，若p%3=2取t=2p，后者仅q=5、k=25不能满足界。素k的2k因子及四个例外逐一排除。 文献/卡点：主全部字段与5个直接ref全部指定字段已读。A343311及另两条重合数列仍以conjecture表述，未见此目标证明；A343311的例外9与本条例外10不同，不能把n≥3的序列相等猜想当已知公式。上面的因子引理与见证是本次分析提出的可检验论证路线，非文献published。open只限所查源与refs。离散分类可绕开计数表，具具体小目标逃逸。 Mathlib：已读Nat.not_prime_iff_exists_mul_eq（Mathlib/Data/Nat/Prime/Basic.lean:85）、Nat.minFac_sq_le_self（Mathlib/Data/Nat/Prime/Defs.lean:368）、Nat.Prime.dvd_mul（同文件:422）；提供因子存在、最小素因子界及素数排除，未给本重合分类。 数值方案：约20行Python筛素数至5000，对每k穷举m=6,9,…,k，用交叉乘积3((2k)%m)==m((2*k)%3)判重合；独立比较k>1且非素且k不在{4,8,10,25}。已实际执行k=1..5000，分类失败为空；此枚举不使用因子构造证明路线或下载表。 全部直接 A 引用：A000040、A002808、A343311、A387426、A389863。

A388986 — precise；dispatch。 精确目标：def U (N:ℕ) := ∑ d∈N.divisors.filter (fun d => Nat.Coprime d (N/d)), d; def S (N:ℕ) := ∑ d∈N.divisors.filter Squarefree, d; theorem euler_form_lt (p a r:ℕ) (hp:p.Prime) (hp4:p%4=1) (hr:Odd r) (hr1:1<r) (hpr:p.Coprime r) : U (p^(4a+1)r^2)+S (p^(4a+1)r^2)<2(p^(4a+1)*r^2). 逃逸：新有限乘积引理：对由≥b>1整数构成的有限集F，Πq∈F(1+1/q²)≤b/(b−1)，用1+1/q²≤q²/(q²−1)并在[b,M]伸缩证明；再按r是否含3以及是否还有其它素因子分三类，同时界住U/N与S/N，不能把U或S定义成所需上界。 文献/卡点：已完整读主源及15个引用，未见Euler形子序列问题的目标证明；open限于这些源。本席给出可实施推导路线（非已发表证明）：p≥5。若r不含3，U/N≤(6/5)(5/4)=3/2且S/N≤(6/5)(6/25)=36/125；若r仅含3，分别≤4/3与8/15，和28/15<2；若r含3及另一素因子≥5，分别≤5/3与(6/5)(4/9)(6/25)=16/125，仍和<2。指数增大只减小归一化因子。所需界全为有限积及有理不等式，不依赖无穷解析。原文2026另一个prime-factorization subset猜想在support解释下被240反例否定，在多重集解释下18与12也否定，故不派该旁支。 Mathlib：ArithmeticFunction.sigma_apply与sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul，Mathlib/NumberTheory/ArithmeticFunction/Misc.lean:151、206，已读声明；NumberTheory内unitary检索仅Pell等无关代数概念，没有此不等式或单位因子和的现成绑定。 数值方案：几十行试除分解1≤N≤10^6，识别恰一个奇指数、该素数及指数均≡1 mod4、其余指数为偶数且r>1；独立枚举因子d用gcd(d,N/d)=1求U，用squarefree(d)求S，与素因子积Π(q^e+1)、Π(q+1)交叉核查并测试U+S<2N。另实测Browne的prime-support版本首个反例为240：U=408,S=72，而210<240且rad240=30∣210并新增素数7。 全部直接 A 引用：A013929、A034448、A048108、A048250、A228058、A325963、A325973、A325977、A360765、A386427、A388985、A389079、A389215、A389217、A389219。

A397345 — precise；dispatch。 精确目标：先在ℚ中定义源a0=a1=1，对n≥2令a_n=5na_(n−1)+nΣ_{j=2..n−1}((5j²−1)/j)a_ja_(n−j)，此递推由A=exp(x+Σ_{n≥2}(5n²−1)a_nx^n/(5n²))逐项求导得到且确定唯一序列。新整数递推b:ℕ→ℕ，b0=0,b1=1，n≥2时b_n=5(n−1)b_(n−1)+Σ_{j=2..n−1}(5j²−1)(n−j)b_jb_(n−j)；证明a_n=(nb_n:ℚ)对n≥1。定义aInt(0)=1,aInt(n)=nb_n(n≥1)；theorem parity(n:ℕ):Odd(aInt n) ↔ ∃k:ℕ,n+1=2^k。系数减法用ℤ/ℚ或依j≥2证明自然数无截断。 逃逸：先证b_(2t)≡b_(2t−1) mod2及b_(2m+1)≡Σ_{t=1..m}b_(2t−1)*b_(2(m−t)+1) mod2；因为模2只剩偶数j，后式恰为Catalan卷积，遂归纳b_(2m+1)≡catalan(m)。再将Catalan卷积非中点项两两交换配对消掉，得C_(2u)偶(u>0)、C_(2u+1)≡C_u，从而C_m奇iff m+1为2幂；处理a偶指标与n=0即可。该整数化→模2→配对归纳是明确的小目标，非只绑定已有通式。 文献/卡点：主全部字段及A397242、A397245、A397346、A397348要求字段已读，均无目标证明链接，同族奇偶性仍称猜想；本轮源与refs未见证明，标open而非穷尽断言。源example已观察n∣a(n)，但未给奇偶证明。整数化递推使分母j完全消去，随后所有模2归约系数可直接核对；独立有限计算支持上述新中间命题，但尚未给Lean证明。未选同页的归一化非零极限猜想，该无界解析题属out。 Mathlib：catalan_succ（Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean:61）给catalan(n+1)=Σi:Fin(n+1),catalan(i)catalan(n−i)，catalan_eq_centralBinom_div（同文件:102）也已读。钉版全树未检得Catalan奇偶定理；即使另有该引理，a/n整数化及模2卷积归约仍须新证，非bind-only。 数值方案：已独立执行n≤200整数b递推：b1=1，b_n=5(n−1)b_(n−1)+Σ_{j=2..n−1}(5j²−1)(n−j)b_j b_(n−j)，a0=1、a_n=nb_n；所有n满足奇偶猜想。同时用Fraction对log(1+Σ_{j<n}a_j x^j)=Σ_{k=1..n}(−1)^(k+1)(Σa_jx^j)^k/k逐阶截断，独立解a_n=−5n²[x^n]log(1+Σ_{j<n}a_jx^j)，前40阶与整数递推完全一致。另用binom(2m,m)/(m+1)核查b_(2m+1)≡Catalan(m) mod2至m=99。核心约35行，无OEIS数据驱动。 全部直接 A 引用：A397242、A397245、A397346、A397348。

A397348 — precise；dispatch。 精确目标：对参数q∈ℕ定义整数序列b_q:ℕ→ℤ，b_q(0)=0、b_q(1)=1，n≥2 时 b_q(n)=q(n−1)b_q(n−1)+∑{j=2}^{n−1}(qj²−1)(n−j)b_q(j)b_q(n−j)，定义 a_q(0)=1、a_q(n)=n b_q(n)（n>0）；由主条目递推令 b_q(n)=a_q(n)/n 可得，须补证与原形式幂级数定义的唯一性对应。 Lean 伪签名：theorem parity_q3 (n : ℕ) : Odd (a_q 3 n) ↔ ∃ r : ℕ, n+1=2^r。 逃逸：拟证从整数递推导出的模2折半律：对 m>0，a_3(2m)≡0；对 m≥0，a_3(2m+1)≡a_3(m) (mod2)。关键是配对卷积并消去交叉项，不是套用 Catalan 奇偶定理；该折半律是拟议、尚未证明的活路径中间命题。 可复用 A397345 段列出的具体中间式：b(2t)≡b_(2t−1)，以及奇指标 b 的 Catalan 卷积；这些模2系数只依赖参数 q 为奇数。三条合并一席，不重复建成果。 文献/卡点：2026-06 Hanna 主条目及五个一跳引用均已读要求字段；相关条目仍把奇偶性标 Conjecture，未提供目标证明或论文。数值由去除分母后的整数递推独立重算。公式(6) nA397349(n)/(n²−1) 与 A397349 的公式(3)冲突：正确换算应是 3nA397349(n)/(3n²−1)，例如 n=2 原式不产6；本分诊不采用该错误式。有关 a(n)/(3^n n!²) 的极限直接 out。 Mathlib：PowerSeries.coeff_exp：coeff n (exp A)=algebraMap ℚ A (1/n!)；.lake/packages/mathlib/Mathlib/RingTheory/PowerSeries/Exp.lean:55。已读声明；只给指数级数基本系数，未命中本猜想。检索 odd/catalan/coeff_exp/valuation factorial，不把无命中说成全库无定理。 数值方案：约30行 Python 按上述 b_3 整数递推计算 a_3，逐项与主条目 data 核对，检验 a(n)%2 == ((n+1)&n==0)。已实际核验 n=0..120 无反例；可扩大至1000，不能据此证全称。 全部直接 A 引用：A397242、A397245、A397345、A397347、A397349。

A397242 — precise；dispatch。 精确目标：设 b : ℕ→ℤ，b(0)=0，b(1)=1，n≥2时 b(n)=(n−1)b(n−1)+∑j∈Icc 2 (n−1),(j²−1)(n−j)b(j)b(n−j)，a(0)=1，a(n)=nb(n)（n>0）；theorem q1_parity (n : ℕ) : Odd (a n) ↔ ∃ r : ℕ, n+1=2^r。另记 n>0 时 (a n%3=1 ↔ ∃r,n+2=3^r∨n+2=23^r) ∧ (a n%3=2 ↔ ∃r s:ℕ,r<s ∧ n+2=3^r+3^s)。 逃逸：与A397348共用一个候选结构引理：奇数q的整数卷积序列在F₂中满足 A=1+xA²；先从原递推导出此式，再读系数得折半律。其证明非指数定义或Catalan定理的绑定；建议合并同族探针，不把q=1、q=3重复作两个独立成果。 可复用 A397345 段列出的具体中间式：b_(2t)≡b_(2t−1)，以及奇指标 b 的 Catalan 卷积；这些模2系数只依赖参数 q 为奇数。三条合并一席，不重复建成果。 文献/卡点：主条目全部字段以及A038464、A397241、A397243要求字段已读；A397241仍把奇偶及模3规律列为猜想，A397243只给对数导数关系，未见奇偶目标证明。模3是同页另一个候选，不作为本次小靶的已证前提。Kotesovec给极限常数数值而未给目标证明；一切极限子问题out。 Mathlib：PowerSeries.coeff_exp，.lake/packages/mathlib/Mathlib/RingTheory/PowerSeries/Exp.lean:55，已读，仅指数级数基础；本地 odd/catalan/coeff_exp 检索未命中该递推的奇偶判别。 数值方案：约30行：b(1)=1；b(n)=(n−1)b(n−1)+sum((j²−1)(n−j)b(j)b(n−j),j=2..n−1)；a(0)=1，a(n)=nb(n)。取n≤120，整数运算后查 a(n)%2 与 (n+1)&n 是否为0；模3部分对n>0用n+2三进制数位判别。方案可执行，本条未另运行。 全部直接 A 引用：A038464、A397241、A397243。

A397346 — precise；dispatch。 精确目标：对参数q∈ℕ定义整数序列b_q:ℕ→ℤ，b_q(0)=0、b_q(1)=1，n≥2 时 b_q(n)=q(n−1)b_q(n−1)+∑_{j=2}^{n−1}(qj²−1)(n−j)b_q(j)b_q(n−j)，定义 a_q(0)=1、a_q(n)=n b_q(n)（n>0）；由主条目递推令 b_q(n)=a_q(n)/n 可得，须补证与原形式幂级数定义的唯一性对应。 Lean 伪签名：theorem residues_q2 (n : ℕ) (hn : 2≤n) : a_q 2 n % 8 = (![4,2,0,2] : Fin 4 → ℤ) ⟨(n−2)%4, by arithmetic⟩。 逃逸：拟证更强的商序列不变量：n≥2 时 b_2(n)≡6(mod8) 若 n≡3(mod4)，否则 b_2(n)≡2(mod8)。将卷积内两端 j=n−1 单列，内部两项都偶而积含4，再按指标奇偶配对计算模8；乘回 n 得原目标。该不变量已在2..120核查，归纳证明待实施。 文献/卡点：主条目和四个一跳引用的要求字段均已读；A397347 的模4陈述也仍是猜想，不能用作既知前提。未见目标证明，故仅按已查范围 open。公式(6)的 nA397347(n)/(n²−1) 应对照 A397347(3)改为2nA397347(n)/(2n²−1)，不照抄。渐近常数猜想 out。 Mathlib：PowerSeries.coeff_exp：coeff n (exp A)=algebraMap ℚ A (1/n!)；.lake/packages/mathlib/Mathlib/RingTheory/PowerSeries/Exp.lean:55。已读声明；只给指数级数基本系数，未命中本猜想。检索 odd/catalan/coeff_exp/valuation factorial，不把无命中说成全库无定理。 数值方案：约30行 Python 计算 b_2(n)、a_2(n)=n*b_2(n)，核对 data 后检查 a(n)%8=[4,2,0,2][(n−2)%4]。已实际算 n=0..120，n=2..120 无反例；并发现 b_2(n) 模8 在 n≥2 时为 n≡3(mod4) 取6、其余取2。 全部直接 A 引用：A397242、A397245、A397347、A397348。

A396804 — precise；dispatch。 精确目标：令 A:PowerSeries ℚ 为 constantCoeff A=0 且 A=X*(PowerSeries.exp ℚ).subst(iterateComp A 4) 的唯一解；iterateComp A 0=X，iterateComp A (k+1)=A.subst(iterateComp A k)。令 a(n):ℕ 满足 (a(n):ℚ)=n! * coeff n A（须独立建立整数性）。theorem mod_four (n:ℕ) (hn:1≤n) : Nat.ModEq 4 (a n) n. 逃逸：拟议新中间命题：对 B=A∘A∘A∘A，所有 n≥2 的整EGF系数 n![x^n]B 都被4整除；用复合的偏Bell多项式递推同时归纳A与B的系数。随后整数Bell多项式的模4相容性给 exp(B)≡exp(x)，乘x导出目标。该中间命题已独立有限核查至n=40，尚需证明全n，不能以主猜想为假设。 文献/卡点：主条目与7个直接引用的全部指定字段均读。旧模3模式[1,2,0]已明确在n=5被反驳；真打开a396804.txt的完整纠错说明和代码，它明确将六周期替代仍标 conjecture，有限核查不是证明。这里选原条目独立的模4猜想，未选已被反驳版本。引用的同族EGF条目只有递推与同类猜想，A000169的Cayley公式属于一次迭代，不能直接覆盖四次迭代。open仅表示这些源和refs未见本模4证明。 Mathlib：PowerSeries.coeff_exp（Mathlib/RingTheory/PowerSeries/Exp.lean）与 PowerSeries.coeff_subst’（Mathlib/RingTheory/PowerSeries/Substitution.lean）已读：给 exp 及复合系数公式，均不直接给EGF整数系数模4周期；Nat.modEq_iff_dvd可作终点接口。 数值方案：已用约35行Python整数EGF算法独立算至n=40：偏Bell多项式递推计算复合四次，完全Bell递推计算exp，按a_n=n·[EGF第n−1系数]迭代40轮。a(n)模4及拟议B=A四次复合的n≥2系数模4均无失败；代码group2/probes.py，收据probes-result.json。可另用Fraction卷积、Horner复合复核，不依赖下载表。 全部直接 A 引用：A000169、A140054、A396799、A396800、A396803、A396805、A396806。

A392714 — precise；dispatch。 精确目标：用一基索引：Φ(n)={σ∈Perm({1,…,2n})：σ(1)=1 ∧ ∀1≤k<2n, Σ_{i=2n−k+1}^{2n}(σ(i)−1−n)≥0}，和在 ℤ 中计算。拟签名 theorem parity_imbalance (n : ℕ) (hn : 1 ≤ n) : (∑ σ ∈ Φ n, signInt σ) = (-1 : ℤ)^(n+1)。有限集合、signInt 和一基到 Fin(2*n) 的转换须在实施时定义；不是已编译签名。 逃逸：拟议逃逸是构造保持所有后缀预算非负的反号对合，并分类其唯一未配对排列。现有求和消去定理不提供这个组合构造；尚未找到/证明该对合。只派一次有停止条件的组合探针，不能把差为1本身当定义。 文献/卡点：Shah–Kiselev, arXiv:2605.11137v1 第3节定义 Φ_p，Remark 4 明确把奇偶差称 conjecture；Claim 4.1 的带权和并未证明这个无权差。A147681 是关联的 late-growing 排列计数，不能因其已出现就降为 published。 Mathlib：Finset.sum_involution（Algebra/BigOperators/Group/Finset/Basic.lean 的 to_additive 生成声明）：只负责已给定反号对合的消去，缺少本有限集上的对合及唯一余项。 数值方案：枚举固定首项为1的 {1,…,2n} 排列（n≤4），从右向左累加 σ(i)−1−n，任一负值即弃；算逆序数奇偶，比较差。应得 n=1..4 的 (偶,奇)=(1,0),(1,2),(18,17),(500,501)；此处只是验证方案与原论文表值，未实际运行。 全部直接 A 引用：A147681。

A370258 — precise；note-only。 文献/卡点：主源确实把形式指数关系标为Conjecture，A102537给出的三角闭式需要行n=m+1、列k=j+1偏移，不能直接同下标替换。A110608的相关指数恒等式及A234839的特殊参数同余不是此目标的证明。已读全部12个直接引用的指定字段；A102537所列Lagrange/Hopf/多边形分割论文全文未打开并建立映射，故unknown。主源另一个微分方程的末项误写R′，不是本次目标。 Mathlib：none（已检索Mathlib/NumberTheory、Combinatorics及RingTheory/PowerSeries中的Lagrange inversion、Gauss congruence等，无目标定理）；PowerSeries.coeff_mul，Mathlib/RingTheory/PowerSeries/Basic.lean:249仅提供卷积基础。 数值方案：用Fraction多项式数组先算Rₖ，再由E₀=1、mEₘ=Σₖ₌₁ᵐRₖEₘ₋ₖ计算形式指数的系数，与给定二项式闭式逐项比较；20余行即可。已独立核查m=0..15全部j，未见反例，记录batch6-numeric.json；可扩大至m=50。 全部直接 A 引用：A000984、A005809、A014105、A026000、A063007、A090763、A090816、A102537、A110608、A114496、A234839、A339710。

A375178 — precise；note-only。 文献/卡点：主源及6个一跳引用完整字段齐读，A112028是移位相同序列，明确p⁵仍appears且Coster Theorem4仅给p³；A176335的已证p^(3r)属于另一平方交错序列，不能移植。本席尝试Coster PDF得到404，Wolstenholme综述也未全文打开，故unknown。所选p⁵是精确有限同余小目标候选，但尚不能满足文献open的派遣门槛。原文另有渐近式按范围out，不选它。 Mathlib：FiniteField.sum_pow_units，Mathlib/FieldTheory/Finite/Basic.lean:290，已读，给有限域单位幂和；Nat.sum_range_choose，Data/Nat/Choose/Sum.lean:94。全库Wolstenholme、supercongruence检索无直接命中；模p⁵的混合调和和消去仍需新引理。 数值方案：对素数7≤p≤199，用math.comb逐k求立方和并模p⁵，与用递推C(p+k−1,k)=C(p+k−2,k−1)*(p+k−1)//k计算的整数结果交叉验证；同时测试p=5以验证排除门槛。只需不到40行。高次支线可测p=7,r=2的49项，但与所选素数级目标分开。 全部直接 A 引用：A000984、A010763、A112028、A176335、A375179、A375180。

A382590 — precise；note-only。 文献/卡点：完整打开 StackExchange API 返回的原问题及全部答案。原问题列 k=2,N=2 的周期(3,5,7)，明确使用不同质因数；Terry Tao 答案490348逐步模aₙ计算出aₙ₊₃≡0，Somos答案490382还给整式因子分解。该整除论证与递增集合/自然数下降链停止即给周期3。初值2非零性可由模5、7有限轨道完整检查：n≢0 mod3 时模5非零；n≡0 mod3 时模7非零（有限初段亦非零），此次已实算循环。打开的 arXiv:2608.11941 附录A A382590 把因子按重数计并证明最终恒2，属于另一口径，不能替代原MO目标。另存模35的完整状态证书：前周期7、周期24，所有状态的a坐标非零；证明定位为该API中answer_id=490348与490382。 Mathlib：Nat.mem_primeFactorsList_iff_dvd（.lake/packages/mathlib/Mathlib/Data/Nat/Factors.lean:143）：n≠0、p素时 p∈primeFactorsList n ↔ p∣n，已读声明。还检索 Dynamics/PeriodicPts/Lemmas.lean 的有限轨道声明；均不直接含三步整除和排序后稳定结论。 数值方案：约35行 Python 用四整数状态生成前25项，以试除/可靠因式分解取去重排序质因数并记录 k=2,3,4；大项增长极快，扩展时改为对有限小素数同时迭代模p状态，但必须把“未找到第k个”标为未知。已独立枚举模5、7完整状态轨道：前周期3、7，周期12、24，检查所有过渡及 aₙ 模5或7至少一者非零；可用几十个小整数作非零证书。 定位：https://api.stackexchange.com/2.3/questions/490330/answers?site=mathoverflow&filter=withbody。 全部直接 A 引用：none。

A392197 — precise；note-only。 文献/卡点：已完整读主源及19个一跳引用。实际打开Höft 2026手稿：p.2 Theorem 1证中央相遇⇒d₊=2d₋+1；p.4 Corollary 3证全部宽1⇒奇因子数=块数；p.3 Corollary 1点名A392197，但不能将两个单向陈述冒充整个集合等价的双向证明。A174905有无保留的宽1等价描述，A298856有中央相遇的另一刻画及完整论证，但尚未打开足以闭合所选完整双向目标的几何证明，故unknown。有限奇核链引理看起来很小，文献桥未确认前不派。 Mathlib：none：钉版Mathlib/NumberTheory文本检索dense divisor、symmetric representation未找到SRS或2-稠密块声明；Nat.divisors只是基础设施。 数值方案：对1≤m≤2000直接枚举升序因子，在相邻比例>2处断开；分别数奇因子，取d₋=max{d∣m:d²≤m}, d₊=m/d₋。独立从Dyck边界构建SRS网格，检查各宽度及中央交点；先不要把待证因子条件用作几何端定义。 定位：https://oeis.org/A237270/a237270_4.pdf#page=2；https://oeis.org/A237270/a237270_4.pdf#page=4；https://oeis.org/A298856。 全部直接 A 引用：A001227、A014105、A033676、A033677、A071561、A162348、A174905、A191363、A237270、A237271、A237593、A250068、A262259、A262626、A264104、A280940、A298856、A384222、A384225。

A394791 — precise；note-only。 文献/卡点：Höft 2026-03-21 Theorem4 的完整证明已解“部分数=最大2-稠密因子块数”，Theorem1(c,d) 证明中心相接⇒中央因子 d₂=2d₁+1 并点名 A298856；A298856 另有其 Dyck 路径刻画的完整双向论证。但将 d₂=2d₁+1 反向推出中心相接的桥，所读证明未明确单独闭合，不能把这些单向结果合称整个枚举猜想已证。故全目标 unknown，先补文献/几何桥，不直接派实施。A384149 的2025-06-27七页手稿 Theorems2–4也已读，仅用其已证部分。 Mathlib：none：几何编码/稠密块桥未在钉版 Mathlib 找到；一旦输入该公开桥，第 n 个相等仅为集合改写，故中风险。 数值方案：试除取得因子排序、在 next>2·previous 处断块并检查两中央因子；另一侧用 A237593 两条 Dyck 路径的网格边界计部分、检测中央相接，扫描小整数直到所需列/最小项，不能两边都用断块公式。 定位：https://oeis.org/A237270/a237270_4.pdf；https://oeis.org/A384149/a384149.pdf；https://oeis.org/A298856。 全部直接 A 引用：A000203、A014105、A033676、A033677、A071561、A174973、A191363、A207375、A237270、A237271、A237593、A239929、A240062、A245092、A262259、A262626、A264104、A280107、A298856、A320511、A384222、A392197、A395156。

A394906 — precise；note-only。 文献/卡点：已读主源和A185101/A007924/A049345所有要求字段，并实际下载/完整读David Dewan的两页Conjectures Notes（2026-04-05）。第三猜想仅给n≤10^8实验和假设Goldbach的重写理由，并非证明。首个“任意非零数字数”猜想在主comment有Hasler完整素数间隙构造；全定义性notes给弱Goldbach论证，但这两项不推出本次选的digit bound。open仅针对选中命题及已查资料。 Mathlib：Nat.exists_prime_lt_and_le_two_mul（.lake/packages/mathlib/Mathlib/NumberTheory/Bertrand.lean:222）已读，给n<p≤2n；Nat.ofDigits_digits（Data/Nat/Digits/Defs.lean:242）给数位转换。它们不直接处理最大表示、余数1的禁区与重复素位的交换，未命中精确digit bound。 数值方案：约25行有界背包DP，以素数pᵢ为重量、10^i为价值，每个权重允许0..9份；对每个金额≤N保存最大整数价值或None。这样完全枚举最优表示而不假定源的贪心程序正确。已计算N=1000，所有主data匹配，n2..1000均有表示且无数字界反例；可扩到10^4，注意价值有π(N)位，避免只用机器整数。 全部直接 A 引用：A007924、A049345、A185101。

A395156 — precise；note-only。 文献/卡点：Höft 2026-03-21 Theorem4 的完整证明已解“部分数=最大2-稠密因子块数”，Theorem1(c,d) 证明中心相接⇒中央因子 d₂=2d₁+1 并点名 A298856；A298856 另有其 Dyck 路径刻画的完整双向论证。但将 d₂=2d₁+1 反向推出中心相接的桥，所读证明未明确单独闭合，不能把这些单向结果合称整个枚举猜想已证。故全目标 unknown，先补文献/几何桥，不直接派实施。A384149 的2025-06-27七页手稿 Theorems2–4也已读，仅用其已证部分。 Mathlib：none：几何编码/稠密块桥未在钉版 Mathlib 找到；一旦输入该公开桥，第 n 个相等仅为集合改写，故中风险。 数值方案：试除取得因子排序、在 next>2·previous 处断块并检查两中央因子；另一侧用 A237593 两条 Dyck 路径的网格边界计部分、检测中央相接，扫描小整数直到所需列/最小项，不能两边都用断块公式。 定位：https://oeis.org/A237270/a237270_4.pdf；https://oeis.org/A384149/a384149.pdf；https://oeis.org/A298856。 全部直接 A 引用：A000203、A014105、A033676、A033677、A071561、A191363、A207375、A237270、A237271、A237593、A240062、A262259、A262626、A264104、A280107、A298856、A320511、A384222、A392197、A394791。

A396836 — precise；note-only。 文献/卡点：主条目与全部一跳引用要求字段已读；两条零限制序列及四条一限制亲缘序列都仍标覆盖性conjecture，仅有数据表/图像，没有目标证明。旋转或反射螺线保持马步，固定右上左下为明确实现。全1的新整数总可继续，故局部贪心确有无限延拓；surjectivity仍需额外论证。这是离散覆盖命题，未按解析无穷性误剔除，但目前只作note-only。 Mathlib：Nat.ofDigits_digits（.lake/packages/mathlib/Mathlib/Data/Nat/Digits/Defs.lean:242）与 Nat.digits_zero（同文件:84）已读；前者给数位解码，后者提醒Mathlib把0写成空列表，必须补[0]约定。全库检索 knight/square spiral/A396836 无目标覆盖性定理。 数值方案：约45行 Python 生成坐标(0,0)起向右、上、左、下，步长1,1,2,2,…；保存已用整数、已有零格集合及下个格索引。从最小未用数逐个试bin(m)[2:]，逐个新零检查8个马步邻格，包括本候选先前新零；通过才整字提交。已独立生成前100项且与全部主data一致；可扩至5000并追踪最小遗漏数，有限遗漏不作反例。 全部直接 A 引用：A007088、A396603、A396604、A396607、A396608、A396837。

A396837 — precise；note-only。 文献/卡点：主条目与全部一跳引用要求字段已读；两条零限制序列及四条一限制亲缘序列都仍标覆盖性conjecture，仅有数据表/图像，没有目标证明。旋转或反射螺线保持马步，固定右上左下为明确实现。全1的新整数总可继续，故局部贪心确有无限延拓；surjectivity仍需额外论证。这是离散覆盖命题，未按解析无穷性误剔除，但目前只作note-only。 Mathlib：Nat.ofDigits_digits（.lake/packages/mathlib/Mathlib/Data/Nat/Digits/Defs.lean:242）与 Nat.digits_zero（同文件:84）已读；前者给数位解码，后者提醒Mathlib把0写成空列表，必须补[0]约定。全库检索 knight/square spiral/A396836 无目标覆盖性定理。 数值方案：约45行 Python 生成坐标(0,0)起向右、上、左、下，步长1,1,2,2,…；保存已用整数、已有零格集合及下个格索引。从最小未用数逐个试bin(m)[2:]，逐个新零检查8个马步邻格，包括本候选先前新零；通过才整字提交。已独立生成前100项且与全部主data一致；可扩至5000并追踪最小遗漏数，有限遗漏不作反例。 全部直接 A 引用：A007088、A396603、A396604、A396607、A396608、A396836。

A397245 — precise；note-only。 文献/卡点：A038464只定义不同3次幂之和；A396846仍称模3规律为猜想；A397242、A397244给系列变换而无目标证明，全部要求字段已读。OEIS无保留递推可用于生成项，不能据其出现就判 published。主条目公式(5)的换算分母 n²−1 与同页 example 的 (4n²−1)/(4n) 关系不一致，正确逆式为4n*A396846(n)/(4n²−1)；example 把 B 系列一处叫 A397241、另一处叫 A397244，暂不采用该混名桥。无界渐近部分 out。 Mathlib：PowerSeries.coeff_exp：coeff n (exp A)=algebraMap ℚ A (1/n!)；.lake/packages/mathlib/Mathlib/RingTheory/PowerSeries/Exp.lean:55。已读声明；只给指数级数基本系数，未命中本猜想。检索 odd/catalan/coeff_exp/valuation factorial，不把无命中说成全库无定理。 数值方案：用 b_4 整数递推计算0..120；把n+2转三进制：恰一个1或恰一个2时应为1，恰两个1时应为2，其他应为0。已独立核查并匹配 data，未见反例；代码用 divmod 实现三进制，不读取OEIS判定结果。 全部直接 A 引用：A038464、A396846、A397242、A397244。

A397340 — precise；note-only。 文献/卡点：主全部字段及7个直接refs全部指定字段已读；真打开Sloane 2017 Properties of A280864完整论证，Theorem3.1给原始A280864包含每素数与每偶数，但其定义允许素数及素数幂，证明还利用2^r，不能绑定当前限制为squarefree composite的变体；OEIS亦标该附件obsolete待重写。当前目标在主源仍为Conjecture，所查源/refs未见变体证明，故open只为本轮有界文献状态，不表示穷尽。 Mathlib：Nat.squarefree_iff_prime_squarefree（Mathlib/Data/Nat/Squarefree.lean:47）把Squarefree n改写为∀p,Prime p→¬p*p∣n；Nat.squarefree_iff_factorization_le_one（同文件:74）已读，只提供质因数指数接口。none for此贪心历史不变量或no-block结论。 数值方案：已实际执行：独立最小素因子筛及p²倍数筛至10^6，初始化used={1},i=j=1；每步W=gcd(i,j),R=j/W，从R的正倍数递增寻找未用、非素、squarefree且与W互素的k，加入used并令(i,j)=(j,k)。得前10,000项、最大选值49,322；9,999对相邻项无互素对，前59项与主data一致。约40行核心代码；候选超筛界须扩大并重筛或记未决，不能当不存在。 全部直接 A 引用：A001221、A002808、A005117、A120944、A280864、A338444、A397127。

A397757 — precise；note-only。 文献/卡点：主全部字段及A331968、A360917要求字段读完；真打开Blondin Massé–Goupil arXiv:2606.13155全部9页（EPTCS445,2026,29–37，DOI10.4204/EPTCS.445.5）。Theorem2明确仅h=1..5，第8页未报告更大高度；不能映射h=6。OEIS Howroyd 2026-07-13称“formula is correct…confirmed via transfer-matrix method”并列递推/GF，但未提供矩阵或完整状态覆盖论证；从该GF可代数推出公式，却不能仅凭同页断言证明其系数真等于最优蛇长。因此文献unknown、note-only，不冒称published或新开放。 Mathlib：SimpleGraph.Subgraph.IsInduced（Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:216）及SimpleGraph.Walk.isInduced_toSubgraph（Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean:350）已读，后者将路径子图诱导性改写为无弦性；只提供图接口，无宽6最优面积定理。 数值方案：约40行Python构造顶点(r,c),0≤r<6,0≤c<n及曼哈顿距离1的邻接位掩码；对n=1..4枚举2^(6n)个非空子集，以位运算检查诱导边数=顶点数−1、每点度≤2、连通，取最大顶点数，独立复核初值6,9,14,17。n=4已有约1678万个子集；n≥7穷举指数增长，不能把n≤4冒充已核验所选n>6通式。后续可做宽6边界DP，状态必须记录6个边界点占用/度数/连通分量与已封闭分量、路径端点计数。 全部直接 A 引用：A331968、A360917。

A377727 — precise；note-only。 文献/卡点：主条目和A267013/A376918/A164864/A266991及comment直接引用A266946的全部要求字段已读。实际打开arXiv:2410.21427完整HTML并读第6节定义、表6和表后论证；表列k2/3的14位362、15位363、16位1444+4，但随后明确说总数是assuming contributions with k>3 are zero的conjectured terms。小概率不是排除证明，故目标literature=open。有限n14..16计数是尚未算尽前沿而非普通一个合数模式正向证书；论文的其他渐近猜想不纳入。 Mathlib：Finset.card_filter_eq_zero_iff（.lake/packages/mathlib/Mathlib/Data/Finset/Card.lean:307）：过滤后card=0 iff每个元素不满足谓词，已读；Nat.ofDigits_zmodeq（Data/Nat/Digits/Lemmas.lean:279）给位权同余，已读。都只支撑有限穷举和整除规则，未命中这些模式精确计数。 数值方案：约50行以restricted-growth strings递归枚举n位模式（首符号0，每个后符号≤前面最大值+1，总符号≤10）；计算各符号位权Cj，按formal排除。对剩余模式枚举0..9的单射赋值且首位非0，逐个组成整数并精确判素；遇一个素数即排除该模式，若全合则保存每个赋值的因子证书。n≤9可完整复现0；n10先做2符号复现3种。真正n14前沿还必须穷尽4..10符号，约1.9亿候选量级，不能把已算2/3符号当完备。64位确定性素性或可验素性证书适用n14..16。 全部直接 A 引用：A164864、A266946、A266991、A267013、A376918。

A398550 — precise；note-only。 文献/卡点：主条目和A378322/A398549全部要求字段已读。主源仅称n4..7穷举；A398549的有限性理由d≤S/r确实给有限递归，但不证明贪心最优；n8解数仅Monte Carlo估计。下界的完整分式变换1/q−w/(wq+1)=1/[q(wq+1)]已核对，不能当成极值上界。无目标证明文献链接，open限此检索。 Mathlib：Finset.sum_le_sum（.lake/packages/mathlib/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:108，由prod_le_prod’的to_additive生成）逐项不等式求和；已读声明/对应文档。NumberTheory/Combinatorics检索Egyptian、unit fraction无本加权互异分母极值定理。 数值方案：约30行精确Fraction深搜：把分母从小到大分配，并枚举其对应的剩余权重w；剩余和r>0、剩余权重总和S时下一个分母d≤floor(S/r)，且d≥上一分母+1、w/d<r（非最后项）；最后一项由d=w/r唯一决定。已完整重算n=1..4，解数1,1,3,44，最大分母1,2,6,60；重算n8贪心见证值与源一致。n8树极大，A398549给约8.4万亿解的蒙特卡洛估计，几十行可定义独立枚举但不表示能在小预算跑完。 全部直接 A 引用：A378322、A398549。

A352656 — precise；note-only。 文献/卡点：主条目 Conjecture 3 无歧义；Conjecture 1 写 p^(4*k) 而 k 未绑定，不能静默改作 r。所有7个直接引用字段已读。真打开 Amdeberhan–Moll 2011 全文6页：定理1.1比较 TSPP 与 ASM 的2进赋值，定理2.1是 SPP=TSSCPP×TSPP；均不能映射到 n×n×2n 的全素数超同余。相关 Wolstenholme/超阶乘论文未完整打开核验，故文献状态 unknown，不凭 MacMahon 计数公式或相邻条目重复猜想拔高 published。强超同余需研究线。 Mathlib：Nat.superFactorial、Nat.prod_range_succ_factorial、Nat.superFactorial_four_mul（Mathlib/Data/Nat/Factorial/SuperFactorial.lean）；Nat.modEq_iff_dvd（Mathlib/Data/Nat/ModEq.lean）。已读声明，只有乘积重写与同余接口，无本目标超同余。 数值方案：约30行 Python：用 factorial 和 Fraction 计算 ∏_{i,j=1..m}(2m+i+j−1)/(i+j−1)，断言分母1；枚举 p∈{2,3,5,7},n=1..4,r=1..3 且 np^r≤120，以大整数模幂检查差。另以超阶乘比复核小 m≤12；普通通过只作探针。 全部直接 A 引用：A000178、A000984、A005809、A008793、A074962、A342972、A352657。

A352657 — precise；note-only。 文献/卡点：主源两项确为猜想，选择带p次幂的Conjecture2，未把右边误写成a(np^(r−1))。5个直接引用的指定字段全部读齐，A008793、A352656同样重述强同余且不提供证明；A352656一般式的4k另有未定义k笔误，未用于本目标。已完整打开Amdeberhan–Moll2011六页《Arithmetic properties of plane partitions》，Theorem1.1及2.1证明的是对称平面分拆/ASM的2-adic估值和乘积关系，不是任意p的盒计数强同余。MacMahon整数性、Krattenthaler行列式枚举本身也不蕴含该模p^(4r)结论；其全文未打开建立额外桥，故unknown。源的渐近公式直接范围外，未选为目标。 Mathlib：Nat.superFactorial及Nat.prod_range_succ_factorial，Mathlib/Data/Nat/Factorial/SuperFactorial.lean:28、66；已完整读该文件声明。Mathlib的sf(m)是1!⋯m!，源S(n)=sf(n−1)（n=0另置1），不可错位。未检出plane partition、lozenge或该p^(4r)同余定理。 数值方案：预计算S(m)=Πⱼ₌₀ᵐ⁻¹j!，用divmod取得a(N)=S(N)^2S(3N)*S(5N)/(S(2N)*S(4N)^2)，每次断言余数0；再算差模p^(4r)，无需在模环中除不可逆分母。已验p∈{2,3,5,7,11,13,17,19}、n=1..5、r=1..4且np^r≤100的70组，两种猜想均通过，并以双乘积交叉核查N=1..15，见batch8-numeric.json。独立组合核查可枚举长度N、元素0..3N的弱降行，以前后行逐坐标支配关系作N层DP；N≤3足够核对真正平面分拆计数。 分工席收尾已实际执行独立弱降行 DP，N=1,2,3 的计数为4、336、572572，与乘积一致；没有将该小范围核查提升为超同余证明。 定位：https://www.combinatorics.org/ojs/index.php/eljc/article/download/v18i2p1/pdf — pp3–5 Theorems 1.1、2.1及证明已读；仅证另一类对称分拆的估值/乘积关系，明确不作为本目标published依据。 全部直接 A 引用：A000178、A005810、A008793、A074962、A352656。

A357506 — precise；note-only。 文献/卡点：主源及7个直接引用完整指定字段已读。Straub2014 Example3.4的确处理同一个B(n)及其移位，但只给p^(3r)，不是选定的p^(3r+3)。已读Bala2022完整两页，表C2(b)直接写出本产品而仍称conjectural。A357508/A357509的Helou–Terjanian已知结果是普通二项式线性组合，未打开其全文并建立到本双Apéry产品的映射，故unknown。数值核查没有改变文献档位。 Mathlib：none（全Mathlib检索Apéry/Apery、supercongruence无目标声明）；Nat.modEq_iff_dvd，Mathlib/Data/Nat/ModEq.lean:111只提供同余表达转换，不提供额外精度。 数值方案：用整数math.comb逐项累加B(n)，缓存后计算B(n)^3*B(n−1)，模幂比较c(p^r)与c(p^(r−1))。已核查p≥5、r=2,3且p^r≤400的8组；另验p=3..101的25个素数的一层c(p)≡27模p^5猜想，均通过，记录batch7-numeric.json。几十行即可扩到最大指标1000。 全部直接 A 引用：A005258、A212334、A339946、A352655、A357507、A357508、A357509。

A357507 — precise；note-only。 文献/卡点：14个直接引用指定字段已齐读，包括A212334的线性组合及A357508/A357509中已证明的普通二项式旁例。Bala2022两页全文的C1(b)逐字列A(n)^5A(n−1)^7，仍作为猜想；Straub论文已读目标相关定理的适用范围，仅保p^(3r)。Adamczewski2026 pp12的证明摘要只处理A357569的两个普通二项式系数，不包含本Apéry产品且并非完整目标证明。其他可能高精度文献尚未打开建立映射，保留unknown。 Mathlib：none（钉版全Mathlib对Apéry/Apery、supercongruence检索无目标）；Nat.modEq_iff_dvd，Mathlib/Data/Nat/ModEq.lean:111只是整除语言桥，普通乘幂同余不会自动增三位精度。 数值方案：用math.comb算A(n)并缓存，直接乘幂后取模，或先把A值模p^(3r+3)再用pow；已验p≥5、r=2,3、p^r≤400的8组。还独立核查p=3..101的25个素数满足c(p)≡3125模p^5。全部通过，batch7-numeric.json；可用相同几十行扩到p^r≤1000。 全部直接 A 引用：A005259、A212334、A339946、A352655、A357506、A357508、A357509、A357567、A357568、A357569、A357956、A357957、A357958、A357959。

A357958 — precise；note-only。 文献/卡点：9个直接引用指定字段全读；已打开Bala两页《Some conjectural supercongruences for the Apéry numbers》全文，C5(a)正是所选线性组合，但整张表明确标conjecturally satisfying，不是证明。Straub已读定理和Example3.4只给单序列及移位序列的p^(3r)精度。邻项Helou/Aidagulov引用针对普通二项式组合，尚未打开全文找到到Apéry组合的证明映射，故保守unknown。原文产品猜想3包含已知p=3反例，不能把产品与主线性组合一并派发。 Mathlib：none（全Mathlib检索Apéry/Apery、supercongruence无相关高阶同余声明）；Nat.modEq_iff_dvd，Mathlib/Data/Nat/ModEq.lean:111仅提供自然数同余和整数差整除的转换。 数值方案：用math.comb独立计算并缓存两类Apéry有限和，取p≥3且p^r≤400、r=2,3逐一验差模p^(3r+3)；已测10组均通过。另验p=5..101的24个素数的一层模p^5猜想。对产品版本u=A^25*B(n-1)^14，已独立复现p=3,r=2反例：v₃(u(9)−u(3))=8<9，余数13122；batch7-numeric.json。 全部直接 A 引用：A005258、A005259、A212334、A352655、A357567、A357956、A357957、A357959、A357960。

A363984 — precise；note-only。 文献/卡点：已读主源及5个一跳引用的完整指定字段，并打开Straub 2014论文，核读pp6–8定理3.1、3.2和Example3.4。3.2(b)的模p^(3r)结论只适用于其特定A_{λ,ε}多项式系数，Example3.4通过特定反射恒等式推出Apéry ζ(2)数的移位同余；目标前项1,3,73并非该数列1,3,19，尚无参数及变换证明可映射。故这篇论文的存在不证明目标，其他潜在证明未打开，判unknown。主源将A363983的有符号和误标A363981，而实际A363981是因子对最小平方条目；已查原文，不随错误xref代入。 Mathlib：none（Mathlib文本检索Apéry/Apery、supercongruence无目标声明）；Nat.modEq_iff_dvd，Mathlib/Data/Nat/ModEq.lean:111只能表达整数差的整除，不能提供3r精度。 数值方案：显式令b(0)=1；k>0用Σⱼ₌₀ᵏ(-1)^(k+j)comb(k,j)comb(k+j-1,j)comb(2j,k)算b(k)，再用Σₖ₌₀ᴺ(-1)^(N+k)comb(N,k)comb(N+k,k)b(k)算a(N)。缓存b，取p=5,7,11、n=1..3、r=1..2，最大N=363，逐个比较两种差模p^(3r)，不调用OEIS数据作真值。 定位：https://arxiv.org/pdf/1401.0854 — pp6–8 Theorems 3.1–3.2、Example 3.4，仅核读适用范围与Apéry特例的反射推导；无本目标映射，非目标证明。 全部直接 A 引用：A000172、A005258、A005259、A363981、A363983。

A380583 — precise；note-only。 文献/卡点：主源和3个直接引用全读；各条都明确把强模数列为conjecture。A380290所述Stanley/Lagrange路线只说明Gauss模p^r；其Notes PDF尝试打开返回403，未能排除其中已处理本题，故unknown。主条目更广u(n)句缺少原本的n倍指数，与本序列定义不一致，所选目标仅用明确a(n)定义。形式幂级数无限积在每次系数上有限，故不是解析out；但所有p,n,r的强提升尚无小路线。 Mathlib：PowerSeries.coeff_mul，Mathlib/RingTheory/PowerSeries/Basic.lean:249，已读卷积声明；全Mathlib文本检索supercongruence、Gauss congruence、Coster无目标命中。Gauss模p^r不能直接绑定为模p^(3r)。 数值方案：只需k≤N截断Euler积到次数N。对每k用整数二项式展开(1+x^(2k))^(Nk²)、(1−x^k)^(−Nk²)，卷积截到N取系数，算a(N)；p=7,11,13，n=1..3、r=1，另p=7,r=2,n=1使N=49。可用log导数递推作第二路线，但若模数下除以j不可逆应先整数精确除再取模。 全部直接 A 引用：A380290、A380581、A380582。

A381460 — vague；note-only。 文献/卡点：主源及15个一跳引用所需字段全读。A379243的公式只给有指定速度的n次幂上界，不控制最小者来自哪类根。主源明确称probabilistic argument且只测至50。后续已完整打开Ripà2024论文（ripa1771.pdf/.txt），Lemma2、Theorem2证明特定底数族的速度与存在性，不证明此处最小值来自±幂等根；2021/2022相关全文未打开，MathOverflow链接尝试返回HTTP403，因此unknown。还存在A373387对2的初始约定冲突；该条生成根的截断层数未在源中量化，故precision=vague并保留研究线。 Mathlib：padicValInt，Mathlib/NumberTheory/Padics/PadicVal/Basic.lean:87；未检出tetration、congruence speed、decadic目标。Mathlib有p-adic设施，但10非素数，不能直接把PadicInt 10当本题所需素数p-adic域绑定。 数值方案：对n=3..8依次扫描整数底数b≥2至首次V(b^n)=n；V用v₂、v₅分支整除计算，n固定时b^n单调故此扫描证最小值。初期可设b≤10^5并报告未找到为unknown。用CRT独立生成e_n∈[0,10^n)满足e_n≡1 mod2^n、e_n≡0 mod5^n，比较b^n mod10^n是否为±e_n；须先确认此截断就是原文generated的意思。 全部直接 A 引用：A018247、A018248、A063006、A091661、A091663、A091664、A120817、A120818、A290372、A290373、A290374、A290375、A317905、A373387、A379243。

A385658 — precise；note-only。 文献/卡点：主全部字段及A000040、A000594、A385676、A385678要求字段均读；主源只称猜想。直接ref A000594的Lehmer相关书目未全部打开到完整证明，因此文献unknown。上述含X因子推导给出目标至少蕴含Lehmer非消失的明确障碍：τ(1)=1使模p后次数不降，τ(n)=0使常数项为0；当n≥3两因子都非单位。现成模形式背景或n≤500表都不证明目标。 Mathlib：Polynomial.Monic.irreducible_of_irreducible_map（Mathlib/Algebra/Polynomial/Eval/Irreducible.lean:44）已读，只给由约化至原环的不可约性方向；none for τ多项式的有界素模数存在或Lehmer非消失。 数值方案：约60行Python以截断整系数卷积计算q*∏_{j=1..N}(1−q^j)^24的q^1..q^N系数，N=40，得到τ；对每n=2..N穷尽p<2n(n+1)素数，以数组多项式快速模幂/gcd实现Rabin判据验证次数n−1的首一多项式。记录首p及此前失败证据，搜空为该n反例；不从OEIS表取τ或候选p。 全部直接 A 引用：A000040、A000594、A385676、A385678。

A385676 — precise；note-only。 文献/卡点：主条目全部字段及A000040、A000203、A385658、A385678要求字段已读；同族仅提出猜想，未见目标证明，open只指本次源与refs检索。n=5的源分解(x+2)(x³+x²+2x+3)两因子均首一，任意素模数仍正度，确实解释该例外，但不能推出其余n均在二次界内有p。n=14首p379等数据不证明全n。 Mathlib：ArithmeticFunction.sigma_one_apply（Mathlib/NumberTheory/ArithmeticFunction/Misc.lean:169）给σ(1,n)=Σd∣n d；Polynomial.Monic.irreducible_of_irreducible_map（Mathlib/Algebra/Polynomial/Eval/Irreducible.lean:44）仅从不可约约化推出原多项式不可约。两处声明已读，无统一二次素数界定理。 数值方案：约50行Python先用除数筛独立计算σ(1)..σ(40)，埃氏筛生成p≤2*40²−40+1；每n穷尽界内素数，对升幂系数[σ(n),…,σ(1)]作Rabin不可约检验：d=n−1，检验X^(p^d)=X mod f，及每个素因子ℓ∣d的gcd(f,X^(p^(d/ℓ))−X)=1；d=1直接通过，n=1常数单位失败。独立实现数组多项式除法、模幂及gcd，记录最小p或全部失败；另展开n=5整数因式分解核验例外。 全部直接 A 引用：A000040、A000203、A385658、A385678。

A386608 — precise；note-only。 文献/卡点：主条目及8个一跳引用完整要求字段已读，另读A377654的partsSRS程序以消歧算法。A249223有宽度的除数半区间解释及周期性证明；A377654有奇素数幂的中心面积公式，但没有给所有n的最小面积实现。主源仍列两个Conjecture。相关背景定理不蕴含本满射，也不能由可能的n²上界反推非空。open只表示这批资料未给目标证明，研究线不自主派。 Mathlib：none（SRS最小面积满射层面）。检索symmetric representation/SRS/Dyck后读 Mathlib/Combinatorics/Enumerative/DyckWord.lean 的DyckWord结构(:65)及equivTreesOfNumNodesEq(:540)，只覆盖Dyck字与树，未给相邻σ边界连通面积或满射定理。 数值方案：约35行按formal的整数天花板和宽度公式生成SRS(k)，扫描k=1..K，对每个最小部分n保存首次k及全部已见k；检查k>n²的反例。已扫描K=10000，全部主data匹配，n1..100皆找到，无扫描范围内k>n²；未找到的n只能记未知，因为尚未证明n²全局截止。两套几何/系数定义的等价还需实施复核。 全部直接 A 引用：A003056、A235791、A237048、A237591、A237593、A249223、A351903、A377654。

A386827 — precise；note-only。 文献/卡点：主全部字段与6个直接ref指定字段已读。通过API真打开MO498716完整问题及唯一回答498719。问题将“Q上不可约”与本文小素数猜想分开；Dotsenko回答给基于Newton多边形的有理不可约论证并引用2019论文，未给n<p<2n(n−1)的p。该论文全文未打开核验，且即便有理结论正确仍不覆盖有界约化；因此文献unknown，不拔高published。 Mathlib：Polynomial.Monic.irreducible_of_irreducible_map（Mathlib/Algebra/Polynomial/Eval/Irreducible.lean:44）已读；它是不可约约化到原环不可约的方向，不能由Q上不可约推出某个范围素模数不可约。 数值方案：约50行Python对n=2..50穷举n<p<2n(n−1)的素数，系数使用pow(k,−1,p)；数组实现乘法/长除/快速模幂/gcd，以Rabin判据验证度数d=n−1的f。对所有ℓ∣d素数检验gcd(f,X^(p^(d/ℓ))−X)=1，最后检验X^(p^d)≡X。记录首个p及此前所有失败原因，搜空则给该n的反例。 全部直接 A 引用：A000040、A385658、A385676、A385678、A386828、A386850。

A386850 — precise；note-only。 文献/卡点：主全部字段与4个直接ref全部指定字段已读；同族A386827/A386828均只标存在猜想。未见本二次素数界的证明，open仅在所查源与refs内。阶乘的定义、exp级数和有理不可约性都不保证有限范围内有不可约约化；每个n有限可判并不使全n结论成为短任务。 Mathlib：Polynomial.Monic.irreducible_of_irreducible_map（Mathlib/Algebra/Polynomial/Eval/Irreducible.lean:44）已读，仅从某个约化不可约推出原多项式不可约，方向不能反用来给指定范围的p；无目标存在定理。 数值方案：约50行Python埃氏筛生成≤(N−1)(2N−1)素数，N=40；对每n与范围p计算k!的模逆作系数。用数组多项式除法、模幂和gcd实现Rabin判据：d=n−1，X^(p^d)=X mod f，且每个素因子ℓ∣d均有gcd(f,X^(p^(d/ℓ))−X)=1；d=1直接通过。穷尽有限p后可严格报告该n存在或不存在，不仅找见证。 全部直接 A 引用：A000040、A000142、A386827、A386828。

A386893 — precise；note-only。 文献/卡点：主条目所有字段已读，直接A号refs为空。真打开van Doorn arXiv:2509.00121全部9页：Theorem1及第2页证明给同一四分支上界，紧接的Conjecture才是n≥92精确等式；Theorem2仅给约n/12下界。又打开Erdős1005网页（2026-09-01更新），其SOLVED对应Ci26证明f(n)=(1/4+o(1))n，不能映射为精确floor加常数；Ci26全文未取得并核验，故选定精确猜想仍标unknown，不冒充published。 Mathlib：none；钉版Mathlib全树检索Farey、farey未找到对应极值对象或精确间隔定理，需自建有限有理数排序及分子分母关系。 数值方案：约40行Python用Fraction约分并排序{a/b:0≤a≤b≤n,gcd(a,b)=1}；对n=4..200按索引差h从1开始检查所有相距h的两项，若分子差乘分母差<0，则a(n)=h−1，立即停止该n。用n≥92的四个余数类别逐项比较；不依赖候选上界停止，必定能枚举至首反例。 全部直接 A 引用：none。

A387421 — precise；note-only。 文献/卡点：主源和8个一跳引用全部字段已读，未见目标证明，open仅指这些源。上述分解说明问题真正剩下powerful完美数；A386428明确说明其奇Euler形特殊素数指数≥5正是Descartes–Frénicle–Sorli猜想排除的一类。A387719仅给必要包含关系，没有证明不存在。因而本条不是普通sigma符号改写的小猜想。 Mathlib：Nat.perfect_iff_sum_divisors_eq_two_mul，Mathlib/NumberTheory/Divisors.lean:401；ArithmeticFunction.isMultiplicative_sigma及sigma素因子积公式，NumberTheory/ArithmeticFunction/Misc.lean:202、206。已读；检索powerful没有目标声明。 数值方案：最小素因子筛到10^6，分解n=Πp^e，计算B=Π_{e≥2}p^e，并独立约数筛计算σ；记录σ=2B的n。还可生成p^(4a+1)r²且a≥1的powerful Euler候选，用因子积交叉检验。小范围无解不是新有限前沿。 全部直接 A 引用：A000203、A057521、A085971、A363169、A378859、A386428、A387420、A387719。

A387947 — precise；note-only。 文献/卡点：主全部字段与4个直接ref全部指定字段已读；Sun2013全文的Theorem1.5只证明另一条A181901的可区分上界，非本目标。另真打开MO501545完整问题和唯一回答501547（has_more=false）：问题给等价合数版本，GH from MO指出n=r²要求两个p≤r²且p≡1(mod r)，当时即使GRH也不能保证该界内一个。回答是难度归约而非目标证明；open限这些已查源。 Mathlib：Nat.Prime.dvd_mul（Mathlib/Data/Nat/Prime/Defs.lean:422）及Nat.Prime.odd_of_ne_two（Mathlib/Data/Nat/Prime/Basic.lean）已读，只能处理平方差因子和奇偶性；钉版无目标素数对存在定理。 数值方案：约30行Python一次筛出≤10000素数，对每n=1..10000将p≤n按(p−1)^2%n分桶；出现第二个素数即得q<p的证书，全部桶大小≤1则a(n)=0。可用sum(c*(c-1)//2)算精确对数；比较零集{1,2,4,9,25}，无需O(pi(n)^2)枚举。 全部直接 A 引用：A000040、A000290、A006093、A181901。

A387959 — precise；note-only。 文献/卡点：主全部字段与5个直接ref全部指定字段已读。完整MO501545正文证明p(n+1)不整除任意平方差：p差过小、p和−2的奇偶性排除；然后将目标化为合数碰撞Conjecture B。唯一回答只指出平方模数的强素数分布障碍，没有证明。Sun2013的A181901对象是交错素数和的平方，本条不能借其定理；open限上述源与refs。 Mathlib：Nat.Prime.dvd_mul（Mathlib/Data/Nat/Prime/Defs.lean:422）、Nat.Prime.odd_of_ne_two（Mathlib/Data/Nat/Prime/Basic.lean）已读，只帮助证明下一个素数是成功模数；没有排除所有更小合数的绑定定理。 数值方案：约35行Python埃氏筛获得前2001个素数；对n≤2000、候选m=n..p[n+1]计算{(p[k]−1)^2%m:k=1..n}，首个基数n的m与p[n+1]比较。也可对候选m缓存首碰撞位置来加速；异常n应分别给1、2、9、25，所有候选有限可完全核查。 全部直接 A 引用：A000040、A000290、A006093、A181901、A387947。

A388012 — precise；note-only。 文献/卡点：已完整读主源及7个直接引用。主源及A388016明确将5/3问题接到Weiner Theorem 3；已打开Holdener 2020页面，但只有摘要，未读其全文或Weiner原文，故unknown而不冒称published。本席可解释条件链：等式给3∣n；若2∣n则6∣n使丰度≥2；奇数n的σ为奇数要求所有素指数偶；若还5∣n则225∣n且丰度≥403/225>5/3；因此5∤n，乘法性给σ(5n)=6σ(n)=10n，即奇完美数。排除此类仍是研究线。另有0.419…密度陈述按用户规则直接out，不派。 Mathlib：Nat.abundancyIndex_le_of_dvd，Mathlib/NumberTheory/FactorisationProperties.lean:204；Nat.perfect_iff_sum_divisors_eq_two_mul，NumberTheory/Divisors.lean:401；ArithmeticFunction.isMultiplicative_sigma，NumberTheory/ArithmeticFunction/Misc.lean:202，已读相应声明。均不能证明5/3不取值。 数值方案：约数筛到10^6，整数比较3σ[n]与5n；加强检验只枚举n=r²、r为奇数、3∣r、5∤r并用试除积求σ，可查r≤10^5。两种枚举小范围交叉验证；有限失败不排除大奇完美数。 全部直接 A 引用：A000203、A353537、A388011、A388013、A388014、A388016、A388017。

A388268 — precise；note-only。 文献/卡点：主源及13个一跳引用字段齐读。主源明确conjectured，A388269、A001599等把它接到Ore数/多重完美数；这些关系不提供目标证明。简单gcd≤最大真因子不能完成，因为主源也指出σ>τ·最大真因子并非总真。A009194所引Pollack的gcd论文及Ore相关全文尚未打开核验，因此保留unknown，不凭论文题目判published或作穷尽open结论。全局gcd消去缺少小目标闭合路线，按必须研究线保留。 Mathlib：Nat.abundant_iff_sum_divisors、Nat.abundancyIndex_le_of_dvd，Mathlib/NumberTheory/FactorisationProperties.lean:195、204，已读；ArithmeticFunction.sigma_apply及sigma素因子积公式在NumberTheory/ArithmeticFunction/Misc.lean。未检出控制gcd(n,σn)与τn的目标声明。 数值方案：双循环约数筛到10^6同时累加τ和σ，每n>1算g=gcd(n,σ[n])并测试τ[n]*g≥σ[n]且σ[n]<2n是否发生；找到反例再试除分解并直接列因子复核。整数交叉乘法避免有理数误差；不能把已有b表当独立枚举。 全部直接 A 引用：A000005、A000203、A000396、A001599、A005100、A005820、A007691、A009194、A017665、A023196、A032742、A388269、A388270。

A389105 — precise；note-only。 文献/卡点：选离散首次出现及下界目标，不选另附的“每个除数无限次出现”（该子句 out）。源报告扫描10^12步后仍未见除数20；只知55个命中到106。首次位置表有问号，不能按连续数列定义全函数后隐藏存在性。A381466 的短递推不构成全覆盖证明，需具名研究方向。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：维护 b(k) 与 gcd，并首次记录各值；可轻验前17项，但连 n=20 的正例都超已报10^12范围，故“有意义的小 n 完整验证”记 no；不能只对已找到项核对后称验证整条。 全部直接 A 引用：A381466。

A389364 — precise；note-only。 文献/卡点：主条目与全部8个直接引用要求字段已读；实际打开作者Not trivial terms with chains文本，核对尾部9723402、74401740及其完整链，材料没有全局排除证明。A114440的有限性断言涉及最终一位数的另一类迭代，当前终点固定两位且digit sum=10，不能转移。A389302记录位置公式也仍为conjecture。主文“really new digits”按紧接的previous terms multiplied by10^x作明确数学化，而非“出现新十进制符号”。 Mathlib：Nat.modEq_digits_sum（.lake/packages/mathlib/Mathlib/Data/Nat/Digits/Lemmas.lean:285）：b’%b=1时n与digits b’ n的和模b相同，已读声明，取b=9,b’=10只给必要同余；未给Harshad迭代根或非平凡种子上界，目标层面none。 数值方案：约30行定义chain(h)：反复以十进制数位和s除h，仅在s>1且s∣h时继续，记录步数和终点；T(h)要求至少1步、steps+2=len(str(h))、终点∈{19,28,37,46,55,64,73,82,91}。扫描至10^6并筛T(h)且(h%10!=0或¬T(h/10))。另可从9个终点逆搜h=sy：给定最多D位只须试2≤s≤9D，检验digsum(sy)=s且h<10^D，再核对depth+2=digits(h)。已独立核对两末种子链及74401740/10不是项、74401740*10是继承项。 全部直接 A 引用：A005349、A007953、A055642、A114440、A235697、A385105、A389235、A389302。

A392498 — precise；note-only。 文献/卡点：完整阅读主条目和6个直接引用，以及真实打开Luschny的ComposableRigidSparse.ipynb全部说明性单元，未见目标证明。对完美数N，Σ_{1<d<L}d=N-1-L。若N偶，则L=N/2，和=L-1<L；若N奇，最小素因子p≥3且L≥p，N-1-L=(p-1)L-1≥L，所以绝不稀疏。完美数不是素数，故目标等价没有奇完美数，不是2026新近小猜想。A000396也明确奇完美数不存在是相信而非已证；未将欧几里得–欧拉偶数分类误用于全部完美数。open仅限此次核查。 Mathlib：Nat.Perfect、Nat.perfect_iff_sum_properDivisors、Nat.perfect_iff_sum_divisors_eq_two_mul，Mathlib/NumberTheory/Divisors.lean:395–403；仅提供完美数定义与σ(N)=2N，不解决奇完美数不存在。文本检索无sparse-perfect目标。 数值方案：约30行因子和筛对N≤10^6独立找Σproper=N，再按最小素因子确定L，试除求Σ_{1<d<L,d∣N}d并比较；可验6,28,496,8128。这只检查已知偶完美数，small N计算不推进未知奇完美数前沿。 全部直接 A 引用：A000396、A392440、A392493、A392494、A392499、A392500。

A392667 — precise；note-only。 文献/卡点：主全部字段与A000040、A000594、A390228指定字段全读。已读Sun2013论文的多项式discriminator定理及证明，它没有τ系数目标；A000594明确将Lehmer非消失及绝对值互异仍列为猜想。其模形式论文和专著未全文核验到本目标，记unknown，不能把τ的已知递推/Deligne界当最小模数证明。因总性已牵涉核心非消失问题，tier3。 Mathlib：none；钉版Mathlib全文检索ramanujanTau、ramanujan.*tau以及discriminator未命中目标声明，τ需从Δ的形式乘积定义并建立接口。 数值方案：约45行Python截断整多项式乘积q∏_{j=1..N}(1−q^j)^24得到τ(1..N)，每因子用binomial(24,t)(−1)^t卷积。对n≤100从m=n逐增，用整数集合查τ(k)(τ(k)−1)模m碰撞，首个成功m试除判素性；先检查整数值是否重复，若重复立即证明该n无任何可区分模数。 全部直接 A 引用：A000040、A000594、A390228。

A392732 — precise；note-only。 文献/卡点：主全部字段及5个直接ref全部指定字段已读。Sun2013的21页论文已打开读完；其中Theorem1.2(i)证明区分k(k−1)/2的最小模数为2^ceil(log2 n)，不是区分2^(k(k−1)/2)；第5节指数discriminator涉及原根的命题被作者明确列为猜想。故所选E(2)精确例外分类未见证明，open仅在所查源范围。原条目极限与无穷多个2幂两部分均out，未拿它们派发。 Mathlib：orderOf_pow’（Mathlib/GroupTheory/OrderOfElement.lean:415）是已读的阶幂公式；钉版discriminator、目标A号检索无最小模数素性分类。 数值方案：约30行Python对n=1..300从m=n递增，计算pow(2,k*(k-1)//2,m)并用集合查重，首个成功模数试除判素性；核查非素n集合是否为{1,3}。设候选m≤10^6，超限为未决；以逐个m完整排除证明每个算出值的最小性。 全部直接 A 引用：A000040、A000079、A000217、A208643、A392775。

A392775 — precise；note-only。 文献/卡点：主全部字段与5个直接ref全部指定字段已读（A000217等长条分段补齐）。Sun2013论文arXiv:1202.6589已打开并分段读完21页；定理1.1及第3节证明的是2k(k−1)及k(k−1)的discriminator，定理1.2处理三角数本身，不能把指数中的三角数当作原多项式。第5节关于指数序列的结论仍是猜想，未见本目标证明；open限这些已查源。另一个m(n)/n→4直接out，未选它。 Mathlib：orderOf_pow’（Mathlib/GroupTheory/OrderOfElement.lean:415）已读，可处理单位群中的指数碰撞；钉版discriminator及目标A号检索无对应最小模数素性定理。 数值方案：约30行Python对n=1..300从m=n递增，以{2pow(3,k(k-1)//2,m)%m:k=1..n}的基数判可区分，首个成功m试除至isqrt(m)判素性；不使用表值。设m≤10^6搜索上限，超限记未决。可将3换成c∈{−13,−11,−5,−3,3,5,11,13}检查n≥abs(c)。 全部直接 A 引用：A000040、A000217、A000244、A208643、A392732。

A393928 — precise；note-only。 文献/卡点：主条目与A000040所有要求字段已读。主引用列Dirichlet1837、Hardy–Littlewood1923、Maynard2015，但这些全文未打开并核对到目标；不凭题名或熟悉的一般结论判published，记unknown。这是精确的离散全称存在命题，按素数分布的核心研究目标保留第三档；未选成短实施靶。 Mathlib：none；钉版Mathlib按目标A号及consecutive primes、complete residue相关文本检索未得此定理；常规Nat.Prime接口不证明连续素数余数模式。 数值方案：约35行Python用埃氏筛生成≤10^7所有素数；对p≤19滑动长度p−1窗口，比较余数集合是否等于set(range(1,p))，首个成功窗口给q及最小性。扫描不够则明确记未找到；更大p所需q可达10^11，不能据有限失败否定存在性。 全部直接 A 引用：A000040。

A394410 — precise；note-only。 文献/卡点：已读五个直接引用的全部要求字段。A056826明确记2013年猜想，2026年更新只是对候选p的计算排除与Aurifeuillean必要条件，非二次递推素数保真的证明。Everest等2003书、Guy A3、De Koninck p51未打开原文，文献状态保守unknown。主条目无保留“连续三项和仅n=1,2为平方”是另一个陈述，不能拿来冒充该质数猜想；不把odd/模8/两平方和等简单性质重证当新小猜想。 Mathlib：Polynomial.cyclotomic_prime，.lake/packages/mathlib/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean:367，已读：素数指标圆分多项式等于几何和；不推出整数代入值为素数。本地 cyclotomic/irreducible 检索未见本递推的质数保真定理。 数值方案：20行生成前10项并用试除或可靠素性库检测较小a(n)；对p=3,5,17,157可构造整数商并用确定性素性证书复核。对后项仅枚举小素数ℓ并算pow(p,p,ℓ)，在ℓ∤p+1时若等于−1可给合数反例。p=a(10)已有62位，p^p存储不可行，不能声称可直接完整核验几十项。 全部直接 A 引用：A000290、A001333、A001481、A002315、A056826。

A394432 — precise；note-only。 文献/卡点：读完主条目所有字段，直接引用A号为空；真打开全部Further notes。附件仅在“此前没有更小n使a(n)=q”等条件下给奇素数幂q首次出现的判据，并列数据，未证明所选严格性猜想。另一个“总为奇素数幂”按字面有a(2)=1例外，未静默修正。open只表示主源及附件未见目标证明；最小性排除仍是研究任务。 Mathlib：orderOf_pow’（Mathlib/GroupTheory/OrderOfElement.lean:415）及orderOf_pow（同文件:996）已读：阶(x^e)=阶(x)/gcd(阶(x),e)，只重写源中的等式，未给最小模数处的严格不等式。 数值方案：约35行Python对e=2..50从r=e²+1起逐个枚举奇数，用x=pow(2,e,r)再反复乘x直到回1求精确阶；首个阶≥e²的r即候选，测试是否等于e²，并保存此前每个r的阶。可预设r≤10^6，未找到记未决；不使用浮点log。 全部直接 A 引用：none。

A394689 — precise；note-only。 文献/卡点：主条目与A064413/A000961/A027748/A392505所有要求字段已读。A000961明确prime power可包含1，故formal显式保留初始1、2而用omega≥2消歧；主example误写a(3)=12，数据实际为6。EKG A064413已有公开覆盖定理，但没有改变交集的限制，不能直接转移；对应EKG论文全文未打开，文献映射尚未完成，故unknown而不说目标已发表。无额外固定点是同页另一观察，本条只选覆盖目标。 Mathlib：Nat.primeFactors_gcd（.lake/packages/mathlib/Mathlib/Data/Nat/PrimeFin.lean:106）：a,b≠0时(gcd a b).primeFactors=a.primeFactors∩b.primeFactors，已读；全库检索EKG/A394689无对应贪心覆盖定理，基础集合等式不解决公平性。 数值方案：约30行 Python 缓存试除得到的不同素因子集，从[1,2]起枚举最小未用m；要求omega(m)≥2，S=pf(m)∩pf(last)非空且不等于上一相邻交集。已生成1000项，主data全匹配，固定点仅1、2；可扩大至10000并列出≤1000的合资格遗漏者。跳过素数幂须先按下述延拓论证解释，不能只照抄前缀。 全部直接 A 引用：A000961、A027748、A064413、A392505。

A395102 — precise；note-only。 文献/卡点：主条目和A065091/A001097/A020484全部要求字段已读；只有主源的n=10000实验支持k=1。相邻双素数与固定差素数表不提供要求两个同时素的区间上界。本条已称奇素数置换并不能推出第三分支的k上界。未见目标证明，open只限上述来源。 Mathlib：Nat.exists_prime_lt_and_le_two_mul（.lake/packages/mathlib/Mathlib/NumberTheory/Bertrand.lean:222）：n>0有n<p≤2n素数，已读声明；它不同时保证q和q−2a(n)为素数，故不能bind证明本猜想。 数值方案：约30行筛素数至100000；从[3]起每步按素数升序选未用q且q%last为素数，完全独立于源的三分支程序。对q≥last且q≠last+2检查q//last==2，遇筛上界耗尽就扩筛而不宣告无项。此次生成1000项，最大12101，主data全匹配且无k>1反例；可扩至10000对照源已测范围。 全部直接 A 引用：A001097、A020484、A065091。

A397155 — precise；note-only。 文献/卡点：A398353 是更广的素数加半素数问题，未给立方子族的证明；这是受限制的加法素数表示目标，尚无明确初等逃逸内容，不自动派实施。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：对 n=2..100 筛至 n³，遍历素数 r<n³，试分解 n³−r 是否恰为两个素数的积（允许 p=q）。 全部直接 A 引用：A000040、A001358、A398353。

A397258 — precise；note-only。 文献/卡点：源 comment 明说“if B lists all and only primes”时等价；A067836 的开放前提没有解除。和 A397259 合并一个研究案，不能把索引换名作为逃逸。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：按 B 递推并维护未见最小素数，计算迟现位置；与有限后缀极小比较，只能作有限诊断。 全部直接 A 引用：A067836、A397259。

A397259 — precise；note-only。 文献/卡点：A067836 的 B 序列“所有素数最终出现”仍是核心前提；A397258 只是相同迟现事件的位置编码。这里要区分可计算的首次出现与依赖全部未来的右向左极小，不能把两个定义强行等同后宣称新定理。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：按 A067836 递推计算 B 的有限前缀，用 seen 集合求迟现素数及位置，并求截断后缀最小；截断后缀不能认证无限未来极小。 全部直接 A 引用：A067836、A397258。

A397260 — precise；note-only。 文献/卡点：S(n)=Σ_{d∣n} digitProduct(d)。例如目标 ∀k≥0 ∀1≤m<8·10^k−2, S(m)<S(8·10^k−2)；其他四族量词范围按源分别 k≥0、k≥1、k>4。A397261 的大项解释只给候选值的贡献下界，未给所有更小竞争数的上界；没有明确全局逃逸。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：用约30行除数筛累加 digitProduct(d) 到所有倍数，算 n≤10^6 的 S 与前缀严格最大值，再测试各数族落入的记录。 全部直接 A 引用：A007954、A093811、A397257、A397261。

A397341 — precise；note-only。 文献/卡点：源给 Bateman–Horn/Schinzel 启发式，MSE 回答5141377也明确是 heuristically，均无证明。源页称“对所有 F≥1 都存在可拼接素数”等价，但该句比仅对递推可达前缀 F 的存在性更强，不能无证明互换。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：逐步按素数从小到大试拼接 F·10^digits(p)+p；小前缀作确定性素性检查并设工作上限，达到上限只报未找到，不能报不存在。 全部直接 A 引用：A000945、A051670、A158191、A167604、A379354、A380010、A397342。

A397369 — precise；note-only。 文献/卡点：精确目标 a(mp^r)≡a(mp^(r−1)) mod p^(4r)，a_n=64^n[z^n]₂F₁(1/4,1/4;1;z)^3，m,r≥1。已打开 arXiv:2605.19773、2604.06238、2606.15462 的主定理，证明的参数分别为 (1/6,1/3) 或 (1/3,1/3)，不是本条 (1/4,1/4)。2110.06768 的一般 eta 算子工具也未给本目标。A393983/A395287 的 level3 证明不转移；属于深层模形式路线。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：以 Fraction 算超几何系数再三重卷积并乘64^n，或用源整数递推；对 p=5,13、m=1..3、r=1..2 且指标≤200 算模幂，交叉核对前缀。 全部直接 A 引用：A393983、A395287。

A397699 — precise；note-only。 文献/卡点：A356840/A397698 给精确算法；已读 Wechsler 的 SeqFan 回答（2026-07-04/05），原文明确说“certainly only a heuristic argument”。故不是 published。他从素数幂删一位再插回的想法未保证不存在更高指数竞争者，尚无全称覆盖证明。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：对每个 n 枚举所有不带前导零的一位插入结果 m，分解各 m；先最大化指数 k，再最大化素数 p，仍同分取最小 m，输出 p。枚举 n≤10000 并记录已出现素数；绝不能按 p^k 的数值大小排序。 定位：https://groups.google.com/g/seqfan/c/1z8o_QY0_AA/m/RRc5YZGiAwAJ。 全部直接 A 引用：A356840、A397698。

A397705 — precise；note-only。 文献/卡点：A046927/A194828 等 Lemoine 相关条目未给带 p<q 限制的全称证明。源页“若 Lemoine 猜想为真则列表完整”没有提供从任意表示到受限表示的推理，不能作 published。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：筛至 B=10^6，对每个奇数 m 枚举 m/3<q≤(m−2)/2 的素数，检查 m−2q 素性并收集例外；可改卷积加速。 全部直接 A 引用：A002091、A002092、A046927、A185091、A194828、A194829、A195353、A195354。

A397711 — precise；note-only。 文献/卡点：源页已有高度分层计数公式的完整论证，并解释素数阶循环重标号；未在完整直接引用找到所有合数 n 的同余证明。目标是 ∀n≥3, card(dag2 n)%n=(若 n 偶则 n/2+1，否则1)。目前仅指出循环群作用方法，尚未得到能推出合数情形的具体固定图分类引理，逃逸路线不够明确，故不派短实施；只证已知素数情形不算完成。 Mathlib：IsPGroup.card_modEq_card_fixedPoints；MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group。前者只给模素数的固定点计数，后者是 Burnside 恒等式，均缺特定 DAG 的合数模数分析。 数值方案：独立枚举 n≤5 的无自环有向邻接位图，检查每点入度≤2并拓扑排序；计数取模。再用源页高度组成递推查 n≤100，仅作第二算法对照。 全部直接 A 引用：A000272、A003024、A243014、A308634、A361718。

A397789 — precise；note-only。 文献/卡点：与 A397790 是同一目标，合并留一个研究任务。相邻素数 u<v 的反例等价于 4q³>(u+v)² 且 2q³<u²+v²。A397790 中的高斯整数论证只排除距离相等，不证明两种最近选择一致；A002821/A077118 的整数邻点公式也不覆盖素数邻点。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：筛 q 及 q^(3/2) 两侧相邻素数，全部以整数比较 4q³、(u+v)²、2q³、u²+v²；n≤1000 无须浮点。 全部直接 A 引用：A000040、A001248、A002821、A030078、A077118、A397790。

A397790 — precise；note-only。 文献/卡点：与 A397789 是同一目标，合并留一个研究任务。相邻素数 u<v 的反例等价于 4q³>(u+v)² 且 2q³<u²+v²。A397790 中的高斯整数论证只排除距离相等，不证明两种最近选择一致；A002821/A077118 的整数邻点公式也不覆盖素数邻点。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：筛 q 及 q^(3/2) 两侧相邻素数，全部以整数比较 4q³、(u+v)²、2q³、u²+v²；n≤1000 无须浮点。 全部直接 A 引用：A000040、A001248、A002821、A030078、A077118、A397789。

A399051 — precise；note-only。 文献/卡点：取 n≥3、N=∏_{j=2}^n p_j，目标 ∃偶数 c，0<c<p_n² 且 Prime(N−c)。A399052 仍称 conjecture；A005235 的 Fortune 类讨论不构成该单侧短区间的证明。未找到可供短实施的素数间隙逃逸引理。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：逐 n 建大整数 N，枚举偶数 c<p_n² 并作确定性试除/素性证书；先做 n≤10，避免把概率素性当精确结果。 全部直接 A 引用：A002110、A005235、A006794、A070826、A399020、A399052。

A359349 — precise；note-only。 文献/卡点：已打开并阅读Davis 2025论文全部10页。p3定理1.4给出同一公式，其上界为B≤3e−7；p7明确将每次半块压缩化为推论3.2，p8–10用补基本对称和估值引理3.3、3.4证明基础定理3.1。取论文m=e即覆盖非平凡区间。OEIS额外的B=3e−6及3e−5均使d=e−1，此时右边指数1且乘积区间与左边完全一致，故完整覆盖原猜想。已读A000722、A067667全部指定字段。本条归out因选定猜想已证明；保留文献线索，不作新猜想dispatch。 Mathlib：none（文本检索未见该奇数乘积块压缩定理）；Nat.modEq_iff_dvd，Mathlib/Data/Nat/ModEq.lean:111及Nat.ModEq.of_dvd:137仅支持转整除与降模。 数值方案：对e=4..16及e<B≤3e−5，用range(2**(e-1)+1,2e,2)边乘边模2B；右边只枚举到2**(e-1)+2d并调用pow(product,2(e-1-d),2**B)。已独立检验195组均成立，batch6-numeric.json。 定位：https://arxiv.org/pdf/2510.22078 — p3 Theorem 1.4；p7 Proof of Theorem 1.4、Theorem 3.1及Corollary 3.2；p8–10完整基础引理证明（本地davis2510.pdf/.txt）。 全部直接 A 引用：A000722、A067667。

A361036 — precise；note-only。 文献/卡点：已打开2026-08-23 v1.3公开论文并完整读12页。Theorem2允许W任意、A,M为保持移位同余的指数；Proposition3给下降阶乘有限和；pp3–5的Lemmas6–7和Section4完整证明逐项模k同余，含超出原求和范围的项。p5 Corollary9取W=1、A=M=id正是源页一般猜想，p6 Example12再取F=G=1+x得到本数列。故published依据是实读证明及参数映射，不是OEIS新增的“true”评论。4个直接引用指定字段已读齐。渐近公式是范围外旁支，未选择。 Mathlib：none（钉版Mathlib无shift-stable/Bala/pseudo-polynomial目标定理）；Nat.factorial_dvd_descFactorial，Mathlib/Data/Nat/Choose/Basic.lean:295及descFactorial_eq_factorial_mul_choose:289是分母吸收基础，不能单独推出目标。外部作者已有同题Lean形式化，未执行。 数值方案：本序列直接用a(n)=Σⱼ₌₀ⁿ(n!/j!)comb(n*(j+1),n-j)整数和计算，不依赖展开器或OEIS缓存数据。已核查所有n≥0,k≥1,n+k≤100的5050对，无失败，记录batch7-numeric.json。一般F,G可用截断整数多项式乘法和论文闭式测试任意给定前100项。 定位：https://github.com/turazashvili/shift-stable-exponents/releases/download/v1.3/paper.pdf — Theorem 2；pp3–5 Proposition 3、Lemmas 6–7及完整Section 4证明；p5 Corollary 9、p6 Example 12（本地turazashvili-paper.pdf/.txt）。 全部直接 A 引用：A047974、A278070、A293013、A361281。

A381005 — precise；note-only。 文献/卡点：主条目完整comment中 Chai Wah Wu（2025-02-13）已直接给完整短证明：令m=2^(2n)、t=2^(2n−1)+1，m为2幂且t奇，故互素异奇偶；三边分别是m²−t²、2mt、m²+t²，因此本原。已打开并读该段（主席成功curl的JSON），并读Mathlib精确分类定理验证映射。Cook博客亦实际打开，但它只给恒等式与二进制性质，未拿它冒充本原证明；Uhler论文未打开，不借其标题判定。因已公开且主要是分类定理代换，档out保留文献。 Mathlib：PythagoreanTriple.coprime_classification（.lake/packages/mathlib/Mathlib/NumberTheory/PythagoreanTriples.lean:524）：整数本原勾股三元组 iff 来自互素且异奇偶的欧几里得参数；已读完整声明和证明。代入 x=2^(2n)、y=2^(2n−1)+1，只有幂式整理和互素性，bind-only风险高。 数值方案：约15行 Python 对 n=1..1000 算三个整数 S,L,H，检查 SS+LL==H*H 及 gcd(S,L)==1；直接平方/欧几里得gcd独立于OEIS数据，也可逐项比对主data。n=1给(7,24,25)；有限正向证书不作为档2前沿。 定位：https://oeis.org/search?q=id:A381005&fmt=json。 全部直接 A 引用：A020884、A381006、A381007、A381008、A381009。

A381006 — precise；note-only。 文献/卡点：主条目完整comment中 Chai Wah Wu（2025-02-13）已直接给完整短证明：令m=2^(2n)、t=2^(2n−1)+1，m为2幂且t奇，故互素异奇偶；三边分别是m²−t²、2mt、m²+t²，因此本原。已打开并读该段（主席成功curl的JSON），并读Mathlib精确分类定理验证映射。Cook博客亦实际打开，但它只给恒等式与二进制性质，未拿它冒充本原证明；Uhler论文未打开，不借其标题判定。因已公开且主要是分类定理代换，档out保留文献。 Mathlib：PythagoreanTriple.coprime_classification（.lake/packages/mathlib/Mathlib/NumberTheory/PythagoreanTriples.lean:524）：整数本原勾股三元组 iff 来自互素且异奇偶的欧几里得参数；已读完整声明和证明。代入 x=2^(2n)、y=2^(2n−1)+1，只有幂式整理和互素性，bind-only风险高。 数值方案：约15行 Python 对 n=1..1000 算三个整数 S,L,H，检查 SS+LL==H*H 及 gcd(S,L)==1；直接平方/欧几里得gcd独立于OEIS数据，也可逐项比对主data。n=1给(7,24,25)；有限正向证书不作为档2前沿。 定位：https://oeis.org/search?q=id:A381006&fmt=json。 全部直接 A 引用：A020883、A381005、A381007、A381008、A381009。

A381007 — precise；note-only。 文献/卡点：主条目完整comment中 Chai Wah Wu（2025-02-13）已直接给完整短证明：令m=2^(2n)、t=2^(2n−1)+1，m为2幂且t奇，故互素异奇偶；三边分别是m²−t²、2mt、m²+t²，因此本原。已打开并读该段（主席成功curl的JSON），并读Mathlib精确分类定理验证映射。Cook博客亦实际打开，但它只给恒等式与二进制性质，未拿它冒充本原证明；Uhler论文未打开，不借其标题判定。因已公开且主要是分类定理代换，档out保留文献。 Mathlib：PythagoreanTriple.coprime_classification（.lake/packages/mathlib/Mathlib/NumberTheory/PythagoreanTriples.lean:524）：整数本原勾股三元组 iff 来自互素且异奇偶的欧几里得参数；已读完整声明和证明。代入 x=2^(2n)、y=2^(2n−1)+1，只有幂式整理和互素性，bind-only风险高。 数值方案：约15行 Python 对 n=1..1000 算三个整数 S,L,H，检查 SS+LL==H*H 及 gcd(S,L)==1；直接平方/欧几里得gcd独立于OEIS数据，也可逐项比对主data。n=1给(7,24,25)；有限正向证书不作为档2前沿。 定位：https://oeis.org/search?q=id:A381007&fmt=json。 全部直接 A 引用：A020882、A381005、A381006、A381008、A381009。

A390228 — vague；note-only。 文献/卡点：主所有字段及3个直接ref全部指定字段已读。源name写c(0),…,c(n−1)，example和Mathematica却用c(k)(c(k)−1)，独立n=4计算确认二者确实不同。Sun2013全文虽证明其他多项式discriminator，却不覆盖j系数；A000521的模形式论文未打开证明本素性目标，故unknown。out源于对象冲突而非否认能计算，note-only保留待订正信息。 Mathlib：none；钉版Mathlib检索Klein.*invariant、jInvariant、j_invariant、目标A号及discriminator无本目标声明。 数值方案：约50行Python用E4(q)=1+240∑σ3(k)q^k及D(q)=∏(1−q^k)^24，做整数卷积和常数项1的级数除法，提取j=q^(-1)E4^3/D的c(0..99)。对原系数和F=c(c−1)分别从m=n起扫描并试除判素性。已用前7个精确系数独立试扫：n=4原系数最小13、二次变换最小16（表为16）；n=6分别19和23。 全部直接 A 引用：A000040、A000521、A392667。

A393833 — precise；note-only。 文献/卡点：主条目、A000005和A032741全部所需字段未见目标证明；open仅限此检索范围。现有Mathlib已证明存在p≡1 mod n；配合素数幂因子公式给出完整本地推导：k的因子正是p^0..p^(2n+1)，共2n+2个；真因子余数全同，故回文。此为当前推导，不冒称目标已有发表证明；因直接绑定足够，排除新靶。主条目example末句a(9)=19^4*37^3与data的19026866不一致，不依赖该句。 Mathlib：Nat.exists_prime_gt_modEq_one，Mathlib/NumberTheory/PrimesCongruentOne.lean:28（∃p,Prime p∧B<p∧p≡1[MOD n]）；Nat.divisors_prime_pow、Nat.properDivisors_prime_pow，Mathlib/NumberTheory/Divisors.lean:420,506（分别为range(e+1)、range e上的幂映射）。已读声明和证明。 数值方案：30行Python对n=1..50搜索p=1+tn的首个素数（n=1取2），令k=p^(2n+1)，独立试除验证p素性，生成幂0..2n+1并检查约数数目及去末项余数串回文。最小项另用除数筛扫描k≤10^6核对可达条目；超界不声称已求最小。 全部直接 A 引用：A000005、A032741。

A394054 — precise；note-only。 文献/卡点：已完整阅读主条目和全部13个一跳引用。实际打开Höft《Theorems Relating to Conjectures by Omar E. Pol》(2026-03-21)4页全文：p.4 Theorem 4及Corollary 1(a)明确证明SRS(n)部分数等于2-稠密块数，依据p.2 Lemma 1(e)与p.3中心块唯一性；同时打开其依赖A384149的7页全文，Theorems 2–3及p.6 Theorem 4给非中心/中心部分与因子块的对应及面积公式。把点态等式代入m≤n的计数就是目标。另打开AlphaProof Nexus target_theorem_0；它预先用奇因子断口表述定义a，故单独不能证明到原始几何定义的忠实性。这里published指公开证明手稿，未声称同行评审。 Mathlib：none（检索NumberTheory的dense/divisor、symmetric representation、SRS未见目标；最终筛集基数相等仅需逐点等式改写，但SRS几何编码与块双射没有查到Mathlib声明）。 数值方案：约40行Python对m=1..2000试除取得升序因子，计1+相邻y>2x的断口数；另对i=1..r，r=floor((sqrt(8m+1)-1)/2)，算b_i=[m≥i(i+1)/2且i整除m-i(i+1)/2]、c_i=Σ_{h≤i}(-1)^(h+1)b_h，计c_i>0的连续段数R，以2R-[c_r>0]得到几何部分数。逐点比较后累计各k的直方图，不能用断口公式同时算两侧。 定位：https://oeis.org/A237270/a237270_4.pdf#page=4；https://oeis.org/A384149/a384149.pdf#page=4；https://raw.githubusercontent.com/google-deepmind/alphaproof-nexus-results/main/APNOutputs/OEIS/oeis_a237271_conjecture_2.lean。 全部直接 A 引用：A000027、A174973、A237270、A237271、A237593、A239663、A240062、A379288、A384149、A384222、A392987、A394052、A394053。

A395171 — precise；note-only。 文献/卡点：该猜想已被公开反驳：MathOverflow 回答511088（2026-06-14）以 p=3,m=2283 给不同 k 的 gcd；不能作为新反驳靶。Love 的回答511242另证合格 m 的存在，不证明 gcd 恒定。本席补查 p=5：m=2..8 在 k=1 时均 gcd=1，m=9 在 k=1 为121、k=1499为362879；121∣9^5−1 保证9对所有 k 合格，故确实对应最小项。published 在本行专指已有反驳与存在证明，不称原猜想被正面证明。 Mathlib：none；Nat.gcd_dvd_left、Nat.gcd_dvd_right 只供整除接口，不能独自决定本序列最小项。 数值方案：已实际用 Python factorial、gcd、pow(base,exponent,modulus) 复算上述 p=5 反例与最小性排除；不需构造9^7495的大整数。 定位：https://mathoverflow.net/a/511088；https://mathoverflow.net/a/511242。 全部直接 A 引用：A000978、A005384、A393224、A395115、A395286、A395944。

A399155 — precise；note-only。 文献/卡点：A175126 的已知公式 f(n)=(n−lpf(n))/2+1 与 A309892 的已知界 g(n)≤n/gpf(n) 已给出支配事实：写 n=l·r，l=lpf(n)，则 g≤n/gpf(n)≤r≤l(r−1)/2+1=f（n≥2）。published 指这两个公开公式及其直接代数推论，未找到单独发表比较定理的论文；条目另问纤维有限，不据此声称已解。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：试除取得最小/最大素因子，各自从 n 迭代到 0，计步，检查 n=2..10000；约30行。 全部直接 A 引用：A175126、A309892。

A381015 — precise；drop。 文献/卡点：主条目全部字段及6个引用齐读。实际打开并分段读完Ripà 2024全文，p.5 Lemma2及p.6 Theorem2证明的是(10^(t+k)+10^t+1)^c的速度，参数k>0，不能把10^(t+k)悄然设为0当作目标实例。相同LTE论证容易导出目标估值，但未读2022速度公式完整证明，故目标publication状态unknown。原文提到Catalan’s conjecture实为已证Mihăilescu定理的名字，并非新猜想；且10^n+1非幂的全部n不能仅由相邻完美幂一句话推出（n=1要另验），不据此派题。 Mathlib：Int.emultiplicity_pow_sub_pow与Int.two_pow_sub_pow’，Mathlib/NumberTheory/Multiplicity.lean:190、291，已读；分别给奇素数LTE及4∣(x−y)时的2进制LTE。x=10^n+1,y=1在n≥2满足后者的4整除假设，n=1需单独处理；没有幂塔速度定义/桥。 数值方案：对n=1..100算整数A=(10^n+1)^n，连续整除A−1求v₂、v₅并与n+min(v₂n,v₅n)比较；再对n≤5用模10^M的递归幂塔（指数按φ链并保留是否超过阈值）算相邻稳定位数增量。不要构造完整高塔。 定位：https://ojs.acad-pub.com/index.php/JAM/article/download/1771/1076#page=5。 全部直接 A 引用：A121520、A122840、A317905、A372490、A373387、A379243。

A383274 — precise；drop。 文献/卡点：主条目全部字段及唯一直接引用A005259的comment/formula/xref/reference/link全读。实际打开arXiv:2505.02767v4（2026-02-10，Frontiers in Combinatorics and Number Theory 2），读定义(1.1)与p.15–16完整Conjecture 4.7：两种求和均从k=0开始，且仍标Conjecture。OEIS漏掉k=0导致本席反例；Example还误写C(i+j,i)²，而Name/程序/论文为一次幂。论文已发表不等于这些猜想已有证明；所选原文命题已否定，三值literature无refuted选项故unknown并明示此情况。修正版目前所读论文仅是猜想。 Mathlib：Nat.sum_range_choose，Mathlib/Data/Nat/Choose/Sum.lean:94；ZMod.euler_criterion，NumberTheory/LegendreSymbol/Basic.lean:62，已读；全Mathlib检索383274无命中。基础二项式/二次剩余声明不提供该p²双和猜想。 数值方案：用math.comb双循环独立求a(k)=Σᵢⱼ C(k,i)²C(k,j)²C(i+j,i)2^(i+j)，先p≤31模p²计算。已执行p=3：a0=1,a1=13,a2=441；不含a0的普通和模9=4而猜想1右端=5；加权和模9=7而14p/5模9=3。证据已存a383274-counterexample.json。 全部直接 A 引用：A005259。

A387664 — precise；drop。 文献/卡点：主源及7个一跳引用全读。A339313说明每个精确速度的素数存在性可用Dirichlet，但这不证明最小值序列无穷下降/平台。原文明确重复是Conjecture；2021、2022速度论文全文未打开，故目标文献unknown，不将速度公式的已知性移植成平台证明。无穷多目标按用户范围直接out。 Mathlib：padicValInt与padicValInt.of_ne_one_ne_zero，Mathlib/NumberTheory/Padics/PadicVal/Basic.lean:87、94，已读；全Mathlib文本检索tetration、congruence speed、decadic无命中。没有最小素数速度重复定理。 数值方案：筛素数p≤10^7，用连续整除计算v₂(p±1)、v₅(p±1)、v₅(p²+1)，按p mod20分支算V；每发现新速度纪录v，填尚未填的阈值n≤v并检查相邻最小值是否相同。可覆盖n≤6的初始阈值；19、20已到19位素数，不适合逐整数扫描。速度公式需另与模10^M幂塔递归核查。 全部直接 A 引用：A000040、A317905、A337392、A337833、A339313、A373387、A389432。

A389650 — precise；drop。 文献/卡点：已实际打开Cloitre arXiv:2508.02690v2 HTML，读Theorem18及其证明、Conjecture19原文。定理18只证c>c0≈0.5956；同文Conjecture19仍明确列c>C，不能把定理18当更强目标的证明。五个直接引用的comment/formula/xref/reference/link已全读。主源把C定义为limsup后其“a(n)≤c p_n最终成立”字面版本有定义性风险；保留论文实际h(n,c p_n)陈述以避免偷换，仍属无界解析，直接out。 Mathlib：zeta_nat_eq_tsum_of_gt_one，.lake/packages/mathlib/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:223，已读，只给整数参数zeta的Dirichlet级数。检索Golomb/Keller/Nagura/Westzynthius无目标命中。 数值方案：几十行筛前201个素数；对n≤200逐个s=2..p_n，用高精度区间算zeta(s)∏{j≤n}(1−p_j^(−s))−1，判断其是否小于(p(n+1)−1)^(−s)，找最小s；可用∑_{m≤M,gcd(m,p_n#)=1,m>1}m^(−s)加积分尾界 M^(1−s)/(s−1)独立包围，跨阈值才增精度。有限实验不能验证“充分大”。 全部直接 A 引用：A000040、A001223、A002110、A002386、A092526。

A390878 — vague；drop。 文献/卡点：主源及18个一跳引用所需字段已完整读，包括很长的A000041。A176206指定整数k出现p(n−k)次；但目标句未说明重复部分/因子组如何计数。实际打开Höft 2026 p.4 Theorem 4，证明SRS部分数=因子块数；这只解决点态权重。按上述澄清版本可直接有限双计数推导，不能据此声称含糊原句已有发表证明。范围上属于语义未固定或既有结论加权，无适当新目标。 Mathlib：Nat.Partition.partitionWithPartEquiv，Mathlib/Combinatorics/Enumerative/Partition/Basic.lean:236，删除一个指定部分的等价；已读声明及实现。没有SRS/因子块目标；若按A176206的p(n−k)多重性定义右端，则剩余为已知点态等式的加权。 数值方案：先明确右端多重性。可用递归枚举n≤15的整数分拆并记录每个不同部分k出现的分拆数，核查为p(n−k)；再独立枚举k因子块并求和，与分拆DP算p及几何SRS算出的卷积比较。若按所有部分出现次数计数则应是Σⱼp(n−jk)，这能检出语义差异。 定位：https://oeis.org/A237270/a237270_4.pdf#page=4。 全部直接 A 引用：A000041、A174973、A176206、A196020、A221529、A235791、A236104、A237270、A237271、A237591、A237593、A245092、A262626、A336811、A384222、A384931、A390877、A390880。

A392059 — vague；drop。 文献/卡点：读完主条目及A387569、A392055全部指定字段；没有引用目标证明。open仅指所查源未見证明；这里另有完整初等反例：高斯整数z=x+yi被1+i整除 iff x+y偶数，n=1、k=P(1)=1时差为i不整除。对整数a或高斯整数a都已失败。范围out是源表述/同余对象问题；未把定义乘积等同于猜想。 Mathlib：none；钉版Mathlib检索Gaussian.*binomial及binomial.*Gaussian无该周期定理；普通高斯整数环或二项式接口不决定分母与模同余约定。 数值方案：n=1无需长程序：a(1)=空积=1，取实部a=0，binom(i,1)−binom(0,1)=i，其实虚部之和为1，故1+i不整除i。约35行Python用Fraction对高斯数对逐项乘(a+ki−j)/n!，测试是否落在Z[i]及差的实虚部和是否偶数；枚举n≤8、a=0..100、k≤2·所给乘积，区分整数性和同余，分母非整数记未定义。 全部直接 A 引用：A387569、A392055。

A393273 — precise；drop。 文献/卡点：主条目所有字段及唯一直接引用A393281的要求字段已读。主comment只有标准Gilbreath背景、定义良好理由及大跳数值，没有声称本序列为全素数置换等新猜想。A393281仅给三角形递推。故不能把“选出底项不为1的排列”错当解决Gilbreath；按仅定义条目out/drop。open指所查源仍称标准目标为conjecture，非穷尽检索。 Mathlib：Nat.exists_infinite_primes（.lake/packages/mathlib/Mathlib/Data/Nat/Prime/Infinite.lean:33）给任意下界以上有素数，已读完整声明；可用于本条延拓存在性。NumberTheory/Combinatorics检索Gilbreath未命中其底项定理，none（猜想层面）。 数值方案：约25行筛前200个升序素数，对每个长度m≥2前缀反复取相邻绝对差直至一个数，查底项是否1。若复现本条，则每次试最小未用素数q，对已有右边界自顶向底更新x←abs(x−edge)，仅当底项≠1才接受；前100项足够核对规则，后段已知大跳会使暴力扫素数很慢。两项计算不能混同。 全部直接 A 引用：A393281。

A394059 — precise；drop。 文献/卡点：已读 Shiu《Strings of Congruent Primes》JLMS 61(2), 359–373 (2000) 的出版社摘要；明确宣称证明对任意 k 有连续 k 个素数同余于任意给定互素类，并由 Crossref 出版记录及 Freiberg 引言核对。取模6、余数1，任意长常值串内含任意多长度 n 的回文窗口，直接推出本目标；不是“有人提出过”而是命中已发表的支配定理。Shiu 正文 PDF 访问未成功，未声称重审整篇证明。即使忽略该文献，infinitely many 也在本席范围外。 Mathlib：none；钉版Mathlib检索Shiu、palindrom.*prime、consecutive primes未得连续同余素数块定理。 数值方案：约35行Python用埃氏筛列出≤10^7素数并取模6，对n=1..30滑动窗口，比较w==w[::-1]，记录最小起点和总出现次数；或中心扩展同时统计各长度。有限次数不能证明无穷多。 定位：https://doi.org/10.1112/S0024610799007863；https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0024610799007863；https://arxiv.org/pdf/1005.4703。 全部直接 A 引用：A039704、A393703。

A395520 — precise；drop。 文献/卡点：主条目全部字段及A001414、A036349指定字段已读。通过StackExchange API打开MathOverflow 510477完整问题与answers（空数组、has_more=false）。其有界债务定义与例示存在起点口径张力，故未选该vague版本，选首现最终排序。所列Alladi–Erdős、Tenenbaum、Weingartner全文未打开，不能由书目或sopfr模2均匀分布推定目标证明，记unknown。该目标为无界算术间隙分布，按范围out。 Mathlib：none；在钉版 Mathlib 检索 sopfr、primeFactorsList.*sum、目标A号，没有此间隙首现顺序定理。 数值方案：约40行Python用最小素因子筛计算s(1)=0、s(n)=s(n/spf(n))+spf(n)，取1≤n≤10^6中s(n)偶数者的相邻差；用素数筛识别差值并记录first[p]。检查已出现素数对p<q的first[p]>first[q]。未出现值记missing，不能当永不出现；增大界只作实验。 全部直接 A 引用：A001414、A036349。

A395605 — precise；drop。 文献/卡点：主源及A000032/A000040/A008683/A064723所有要求字段已读。完整可核查推导：L(3m)=L(m)^3+3L(m)（m奇；由两根α+β=1、αβ=−1的立方恒等式），设dₖ=L(3^k)，则d₀=1,d₁=4，dₖ≡4 mod9(k≥1)。差分分解给uₖ₊₁=uₖ*(dₖ²+dₖdₖ₋₁+dₖ₋₁²+3)/3。k1时因子8；k≥2时因子≡2 mod3，且u₁=1。因此商始终整数且余数交替1、2，否定原p=3极限。相关文献中未打开本极限的正式证明/反证，故literature=unknown；这是本次从已知Lucas恒等式导出的反证，不声称“已发表”。 Mathlib：Metric.cauchySeq_iff（.lake/packages/mathlib/Mathlib/Topology/MetricSpace/Cauchy.lean:59）给∀ε>0最终两项距离<ε的Cauchy刻画，已读；检索Lucas/Padics只见通用p-adic与其他Lucas命名定理，未命中本商极限。 数值方案：约20行从L₀=2,L₁=1的整数递推/矩阵快速幂独立算L(p^k)，对p=3,7,11及k=1..6检查差L(p^k)−L(p^(k−1))能被p^k整除并记录商modp及modp²。已实算p3的k1..6余数为1,2,1,2,1,2；无限不收敛依下述归纳，而非由六项样本断言。 全部直接 A 引用：A000032、A000040、A008683、A064723。

A396081 — precise；drop。 文献/卡点：源 conjecture 明确要求无限多素数；A381466 的已知递推界/局部整除性质不推出无限出现。按用户无穷性断言排除；不把递推易写当可派实施。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：从 b(0)=4 起，g=gcd(b(k−1),k)，g=1 则加 k，否则置 k/g；筛 p≤B 并检查 b(2p)=p，十几行可验前缀但不证无限性。 全部直接 A 引用：A381466、A394761。

A396696 — precise；drop。 文献/卡点：这是无界实分析及素数间隙存在断言。A051254 的 Mills 定理、A051501 的 Wright 构造及 A082282 使用其他增长尺度，不能替代本猜想；所检索条目未给本尺度的证明。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：以 nextprime 迭代有限前缀 a_n，精确检查 a_n<n²(a_(n−1)+1)，给有限区间交而非实数 C 的全称证书。 全部直接 A 引用：A051254、A051501、A082282。

A396785 — precise；drop。 文献/卡点：主条目及A381466/A381501全部要求字段已读，来源无目标证明链接；A381466给出平方根下界等无保留断言，能解释每个p的有限检索窗口，却不证明有无穷多个p遗漏。A381501线性增长也是经验语句。主目标明确infinitely many，按范围out，不能降格为验证几个遗漏素数的普通有限证书。 Mathlib：Nat.gcd_greatest（.lake/packages/mathlib/Mathlib/Data/Nat/GCD/Basic.lean:35）给gcd的最大公因子刻画，已读声明；全库检索 Rowland、A381466 未见本递推的素数遗漏无穷定理，none（目标层面）。 数值方案：约30行 Python 从 u=4 对 n=1..P*(6*P−2) 顺序迭代 g=gcd(u,n)，g=1则u+=n，否则u=n//g并记录除法步素数输出；筛 p≤P 去掉记录者。P=200即可重现首个17、103等；P=1000约600万步。有限截止依赖OEIS无保留给出的全局值下界/出现位置上界，独立重证前只能将结果标条件性完整；直接记录出现则无此依赖。 全部直接 A 引用：A381466、A381501。

A396847 — precise；drop。 文献/卡点：A119471 的相关实数/级数关系仍为猜想；所查条目未给边界收敛及等式证明。收敛半径与边界取值是本席排除的无界解析断言。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：可截断级数并用有理区间迭代估计根，但没有尾项误差证书就不能检验边界取值，故 no。 全部直接 A 引用：A119471。

A396915 — precise；drop。 文献/卡点：已读主条目和A003415/A005117/A120944所有要求字段。主条目明确只以Bunyakovsky猜想支持无穷性，计数为经验启发。实际打开 erdosproblems.com/307，页面仍标Open且Proof expositions(0)，该题要求两个素数倒数和乘积为1，与本条仅加号平方条件不同，不能把二者等同。无界infinitely many/asymptotic按用户范围直接out；open仅表示所查来源无目标证明。 Mathlib：Nat.squarefree_iff_nodup_primeFactorsList（.lake/packages/mathlib/Mathlib/Data/Nat/Squarefree.lean:34）：n≠0时无平方因子等价于素因数列表无重复；已读声明。全库文本检索 arithmeticDeriv/arithmetic derivative/Bunyakovsky 未命中目标，无直接素值多项式无穷性声明。 数值方案：约30行筛最小素因子至 X=10^6，分解每个k，只保留至少2个不同素因子且指数全1，算 D(k)=Σ_{p∣k}k//p，再以 isqrt(D(k)+2k)^2==D(k)+2k 判入列；核对 data 和计数比值。可另筛 s≤10^4、s≡±4 mod11，检验 q=(s²−5)/11 为素数，得到子族5q。仅有限样本，不能验证无穷或渐近。 全部直接 A 引用：A003415、A005117、A120944。

A398129 — vague；drop。 文献/卡点：列表成员由猜想性的“唯一无限分支”决定；有限前缀不能无条件确定该序列。A398130 是同一树的另一同余类，A078611/A129758 的对称素数定义没有证明无限分支唯一。可以另写精确树谓词，但此无界分支目标不进入本席。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：筛到明确上限，对每个中点找最近对称素数对并建有限树，记录截断处活分支；这不能验证真正的分支成员资格，故 no。 全部直接 A 引用：A002476、A007528、A078611、A129758、A398130。

A398130 — vague；drop。 文献/卡点：列表成员由猜想性的“唯一无限分支”决定；有限前缀不能无条件确定该序列。A398129 是同一树的另一同余类，A078611/A129758 的对称素数定义没有证明无限分支唯一。可以另写精确树谓词，但此无界分支目标不进入本席。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：筛到明确上限，对每个中点找最近对称素数对并建有限树，记录截断处活分支；这不能验证真正的分支成员资格，故 no。 全部直接 A 引用：A002476、A007528、A078611、A129758、A398129。

A398367 — precise；drop。 文献/卡点：读完主条目全部字段及唯一直接引用A398382的全部指定字段。主条目对无界性另有鸽巢论证，但明确写 The convergence to this solution is still conjectural；相位长度恒等式及x方程的theta改写不证明收敛。未见目标证明（open仅在这些源与refs的已查范围内）；两个目标均为无界解析极限，按用户范围直接out。 Mathlib：none；在钉版Mathlib及D5检索 trampled、carousel、A398367 无目标命中；此处没有现成过程极限定理。 数值方案：约40行Python用列表cells=[0]、位置p=0，每步append(0)、cells[p]+=1、记录值并令p=(p−cells[p])%len(cells)；扫描前10^6步切分极大连续1段与>1段，计算L(k+1)/L(k)及均值。方程右侧截到m=30，二分x∈[0.6,0.7]，尾项用几何级数界；有限数据只能比较，不能证极限。 全部直接 A 引用：A398382。

A398812 — precise；drop。 文献/卡点：源 formula 已附 Chai Wah Wu（2026-08-20）的完整夹逼：覆盖面积 A138808(n)≤n·τ(n)，τ(n)≤2√n，故比例亏损≤2/√n→0；本身也属于本席排除的渐近断言。A398810 当前是 allocated 占位条目，无数学字段。 Mathlib：none（在已检索的 Mathlib 范围未找到目标声明） 数值方案：对 n≤100 枚举整数格 (x,y)，覆盖当且仅当存在 d∣n 满足 x≤d 且 y≤n/d，计未覆盖面积；数值 yes 仅指前缀。 全部直接 A 引用：A138808、A283626、A398809、A398810、A398812。

未主张

未主张检索穷尽、open 等于全球无人证明、所有外链论文已全文审读、或 published 等于原猜想为真。未跑 Lean、未编译伪签名、未核验公理闭包、未建模块/原子/冻结记录。未证明任何 dispatch 目标，也未保证其符合最终逃逸准入；具体声明检索不等于真实 bind-only 探针。

仅逐段明确报告已执行的数值检查（包括小反例、前缀复现及模数扫描）算本席实测；其余数值栏均是可执行的验证方案，未声称已运行。文献中的表值和程序输出不冒充本席独立数值证据。A395171 的本席计算：p=5、m=9，k=1 时 gcd=121，k=1499 时 gcd=362879；m=2..8 在 k=1 时均为1。该结果只补充已公开的反驳，未主张新发现或形式化反驳。

未对第三档目标作自主研究承诺；未把有限前缀通过、概率素性、相邻已知公式、外部 Lean 文本或单向蕴含冒充所需的无界精确定理。