对于方程 x + by = bz，R_k(b) 是使每一种 k 色染色都必有单色解的最小区间大小。论文给出已知情形的解析证明、有限可满足性（SAT）检查，以及证明 R_5(3) 大于 296 的显式五色染色。阈值猜想描述何时 R_k(b) 等于 b^k；一般猜想仍未解决。2026 年 9 月更正将已知下界 R_5(2) ≥ 56 正确归于 Chang、De Loera 和 Wesley 的 R_4(2) = 56 结果。研究包含部分 Lean 形式化，并非整篇证明均已由 Lean 内核检查。

SSRN2026-06-03 Zenodo2026-03-11 代码与材料

2026-05-22

组合数学内部定稿工作论文 · Zenodo

Rado 方程 x + by = bz 的距离对刻画：纯内核 Lean 4 形式化

在 Lean 中形式化对应 Rado 阈值方向的距离对机制，并明确保留解析级联假设。

Zenodo2026-05-22 代码与材料

2026-07-12修订 2026-08-31

组合数学 Kernel-Only工作论文 · SSRN

非交叉划分细化图中的 Hamilton 圈与路径

完整分类非交叉划分细化图中的 Hamilton 圈与路径，并给出统一构造和奇偶障碍。

SSRN Zenodo2026-07-12 Kernel-Only 形式化

2026-09-06修订 2026-09-14

数论 Kernel-Only工作论文 · SSRN

合数限制下的可见格点图中的无限路径

图的顶点是两个坐标都大于一的互素整数对，且每个顶点至少有一个合数坐标；相邻顶点间走一个单位步。论文构造无限路径，并对区间 (4/3,5/3) 内几乎每个比值，给出以该值为极限坐标比的无限简单路径。修订稿引用 rafalwrona 的局部行列式观察及 Duncan 的有限路径观察。证明还提供了得到全局定理所需的粗糙合数短带、安全支撑列、同时控制方向的估计及跨尺度连接。

SSRN2026-09-14 Zenodo2026-09-06 Kernel-Only 形式化

2026-09-06修订 2026-09-18

组合数学 Kernel-Only工作论文 · SSRN

加性增广间隙不能保证对数凹性

对独立集的增广规则作固定的加性放宽，并不能保证各个大小的独立集数量呈对数凹性。一个含 13 个元素、秩为 4 的例子给出计数 1、13、25、7、2，反驳了 Xie 与 Xu 的秩相关猜想；进一步的反例族保持同一增广参数，而对数凹性比值趋于零。

SSRN2026-09-14 Zenodo2026-09-06 Kernel-Only 形式化

2026-09-06

组合数学内部定稿工作论文 · Zenodo

次数无界的全实根邻域多项式

邻域多项式按大小计数具有公共邻点的顶点子集。构造任意最大度的树，使其邻域多项式仅有互异负实根，回答 Day 的问题，并完整刻画固定最大度时的系数极限。

Zenodo2026-09-06

2026-09-06修订 2026-09-17

组合数学 Kernel-Only工作论文 · Zenodo

非负分圆多项式乘积与面数为平方数的骰子

分圆多项式以本原单位根为零点。本文完整刻画由两个互异素数的幂确定的一个乘积族何时系数全非负，解决 Fiore–Nasr–Stone 关于面数为平方数的骰子重新标号的猜想 5.7，并证明乘子的最优次数下界及全部等号情形。文中数学结果已有公开的 Lean 4 证明，使用通常的整系数多项式。

Zenodo2026-09-06 Kernel-Only 形式化

2026-09-06

组合数学内部定稿工作论文 · Zenodo

二项式幂和之比的峰值与高斯极限

研究截断二项式幂和与较短行中完整幂和之比。对固定正实数幂和正权重，证明猜想中的渐近最大值，给出平移后的整数峰值位置与高斯极限；平方幂时还证明所有正权重下的严格对数凹性。

Zenodo2026-09-06

2026-09-06修订 2026-09-18

组合数学 Kernel-Only工作论文 · Zenodo

独立集阈值游戏与奇环上的测地移除

测地移除游戏在未选顶点无法通过反复加入最短路径生成固定的原图时结束。对至少含五个顶点的奇环，一个所选集合终止，当且仅当它包含改变循环顺序后所得环的一个最大独立集。利用这一对应，可用动态配对策略证明后手必胜并确定精确获胜步数，且可推广到路径和环上的独立集阈值游戏。

Zenodo2026-09-06 Kernel-Only 形式化代码与材料

2026-09-06修订 2026-09-18

组合数学 Kernel-Only工作论文 · Zenodo

圆柱图的四部分多重集分辨划分

记录顶点到各划分部分的最小距离，不保留部分标签，但保留重复距离。将两条同长的环在对应顶点之间连边所得的棱柱图，在环长至少为十时，四个部分足以区分所有顶点，而且已达最优。显式的环上距离多重集还给出指定圆柱图划分的精确高度边界。五部分上界适用于环长八、九的棱柱图，以及层数至少二、偶数周长至少十二的圆柱图。

Zenodo2026-09-06 Kernel-Only 形式化代码与材料

2026-09-06

组合数学内部定稿工作论文 · Zenodo

填字网格上车摆放的一致稀疏渐近式

完整车摆放在每行、每列的每个极大连续白格区间中恰好选取一个格子。对于均匀选取 k 个黑格的 n×n 网格，当 k 的增长慢于 n 的平方根时，摆放数量的平均值渐近于 n!(n/36)^k。当 k/sqrt(n) 趋于有限值 lambda 时，归一化平均值趋于 exp(-27 lambda^2/50)。连通分支分析还给出均匀网格与摆放配对的空间分布规律，以及均匀网格的摆放存在性界。

Zenodo2026-09-06

2026-09-06修订 2026-09-08

组合数学内部定稿工作论文 · Zenodo

有界占用令牌图中的匹配与独立数：独立并行开发

将固定数量、彼此不可区分的令牌分配到图的顶点，每一步沿一条边移动一个令牌。本文保留对 Reyes、Dalfó 和 Fiol 猜想 3.6 的独立开发证明及有界占用推论。Patel 更早公开的完整解答已用相同构造解决无占用上限情形：固定匹配边上的令牌总数，再在路径的直积上构造匹配。修订稿作为独立并行开发的说明性文章存档，不主张首次解答的优先权。

Zenodo2026-09-06

2026-09-07

组合数学内部定稿工作论文 · Zenodo

稳定连续模式与链簇

连续排列模式规定一段相邻且互异字母的相对次序。我们刻画这样的模式：把各字母的出现重数相互置换，模式出现次数的分布保持不变。判据是每组连通的重叠出现都迫使其全部位置形成唯一全序。论文给出锐的有限出现对计数检验、包括 12435 在内的非单调稳定例子、精确位置分布的推广，以及同长且均以最小字母开头的模式族的联合判据。

Zenodo2026-09-07

2026-09-07修订 2026-09-28

组合数学 Kernel-Only工作论文 · Zenodo

从关联结构识别递归设计

这里的设计由互不相同、等大且至少含两个点的子集组成，这些子集称为区组；每个点属于同一个正数的区组。对于两种递归构造，我们仅从点与区组的隶属关系中恢复隐藏的分部，并确定所有保持区组的点置换，即自同构。这证明了 Amarra、Devillers 和 Praeger 的两个猜想，并分类了例外。隶属向量之间的整数关系还能在事先不知道参数时恢复单分划构造的输入设计。固定的有限构造步骤序列继承相应的群与同构结论。

Zenodo2026-09-07 Kernel-Only 形式化

2026-09-07

分析与概率内部定稿工作论文 · Zenodo

截断 Stieltjes 积分方程的唯一峰值

本文研究由积分方程确定的曲线。对于先上升到一个峰再下降的正剖面 h，若下降一侧的相对斜率 xh'(x)/h(x) 严格递减，则每条存在的曲线都只有一个峰，从而证明 Viakhirev 的唯一性猜想。结论覆盖积分核的所有正幂，确定曲线可存在的精确水平范围及峰的位置如何变化。对于原文提出的归一化对数正态截断，峰的位置与高度趋向不依赖截断指数的极限，并有显式的一阶修正。只有一个峰的光滑剖面仍可能产生驻点任意多的曲线；驻点是导数为零的点。

Zenodo2026-09-07

2026-09-07

组合数学内部定稿工作论文 · Zenodo

顶点标号图的零距离等价类

给连通图的顶点赋非负数，并对连接两点的路径取最大标号、再对所有路径取下确界，就得到一种距离。不同顶点的距离可能为零；这些彼此无法由距离区分的顶点组成零距离等价类。本文刻画哪些指定集合可以成为这样的等价类，证明 Dovgoshey 与 Rovenska 圈猜想的有限类版本，并通过在已知半 Farey 图的每条边上插入一个新顶点来反驳其不受限版本。在这一反例中，任意两点之间内部顶点互不相交的路径至多有三条，且三是可能的最小统一上界。论文还刻画了哪些图在每条边至少有一个端点标号为正的所有标号下，都能分离不同顶点，或都使每个点成为孤立点。

Zenodo2026-09-07

2026-09-07

组合数学内部定稿工作论文 · Zenodo

单射限制均为偶的变换

对有限有序集上的映射，逆序是指一对输入的像以相反次序排列。本文分类如下映射：任取 t 个像互不相同的输入，逆序数都为偶数。具有相同像的输入组成一个块，块数称为秩。所得分块条件回答了 Vítor H. Fernandes 在 arXiv 2605.12342 中提出的两个缺失秩层问题，即秩为 t 和 t+1 的情形。论文给出这些映射及连续作用两次仍与作用一次相同的映射的封闭计数公式，并将分类扩展到部分定义的映射及逆序数为奇数的限制。

Zenodo2026-09-07

2026-09-08修订 2026-10-02

组合数学 Kernel-Only工作论文 · Zenodo

相邻差有界的 132 避免排列：严格增长与下降阈值

若一个排列中不存在三个元素按 132 的相对大小次序出现，就称它避免 132。把相邻数值的绝对差限制为至多 m，所得排列族的指数增长率随 m 严格增加；这一结果在 Mayama 和 Akita 的计数理论基础上，补齐了 Nadler 猜想 2 中剩余的断言。下降是指一个元素大于紧随其后的元素。给每个下降赋予权重后，会出现增长率等于一的区域，以及两种不同尺度的阈值。论文在同一篇中证明了带权增长判据及其极限增长率。

Zenodo2026-09-08 Kernel-Only 形式化代码与材料

2026-09-08

组合数学内部定稿工作论文 · Zenodo

彩色交错三角形的锐化稳定阈值与固定能量规律

深度为二的彩色交错三角形中，每种颜色在上排出现两次、下排出现一次，次序为上—下—上。Patel 更早的完整解答已证明 Blitvić–Petrov 模型的最终系数多项式性和线性累积量。本文细化同一机制，给出全阶最优阈值 n 至少为 2k+1、精确边界偏差、带逆序数标记及空间位置的极限律；下排为恒等次序时，最优阈值改进为 n 至少为 k+1。重复的低阶推导已删除。全局对数凹性猜想 4.1 不在证明范围内。

Zenodo2026-09-08

2026-09-08

拓扑学内部定稿工作论文 · Zenodo

二桥纽结符号差的精确方差与精细极限律

二桥纽结可画成只有两个上桥的图形，其符号差是一个取整数值的纽结不变量。在 Cohen、Baker、Dam、Felber、Madras、Saha 和 Thackrah 使用的词模型中，部分纽结被计数两次。本文确定每个交叉数 c 对应的符号差精确方差，并证明方差减去 c 趋于 -14/3，回答他们在 arXiv 2604.21107 中提出的数值猜想 5.1。论文还给出单个符号差取值概率及罕见大符号差概率的逐阶精细近似。若将互为镜像的纽结视为同一类，均匀选类后独立、等概率地选择符号的正负，就得到另一种对称模型；论文保留精确抽样权重，推导其随交叉数奇偶性变化的方差与概率修正。

Zenodo2026-09-08

2026-09-08修订 2026-10-11

分析与概率 Kernel-Only工作论文 · Zenodo

指数能量的精确构型与碰撞尺度

在一个区间上放置允许重复的点，使各点对距离 d 对应的 exp(-d) 之和最小。论文确定了全部极小位置及每个端点的精确重复点数。在单位区间上，这证明了 Emmerich 在 arXiv 2603.28179v2 第 4 节报告的经验性三分之一规律。论文还在点数和区间长度固定时，回答附录 A.3 末尾关于邻近 q 值的问题。对于 exp(-d^q)，当 q 从下方趋于 1 时，簇内移动点以不同的指数尺度靠近端点；在特殊长度处，最外层尺度转而带有对数修正。当 q 从上方趋于 1 时，端点重数保持不变，包括这些特殊长度。有限尺寸能量修正和各指数尺度共有的领先因子也在同一篇中得到证明。猜想 A.1 和 A.2 中的全局转变不属于本文的局部结果。

Zenodo2026-09-08 Kernel-Only 形式化

2026-09-09修订 2026-09-10

集合论 Reference-Gated · 中间发布版本工作论文 · SSRN

序数图分割关系的非普适性障碍

Erdős 第597题询问，序数平方 ω₁² 的两色染色必然包含哪些图。本文将 Shelah 已有的非普适性定理应用于 Erdős 所报告的 Baumgartner 负分割关系，对不限制为有限目标图的断言给出反例。目标恰有 ℵ₁ 个顶点，是连通二部图，直径至多为三，并且不含可数无限完全二部图。本文给出显式的双团秩证明及连通目标构造，同时明确归属 Shelah 先行的树节点可比较性机制。Lean 配套代码验证图的构造及从引用的 Baumgartner 定理到结论的推导，该引用定理的证明位于代码库之外；Reference-Gated 描述的是这一机器验证边界。有限目标图问题仍未解决。

SSRN2026-09-10 Zenodo2026-09-09 Reference-Gated 形式化代码与材料引用关口：命题与来源

2026-09-09

组合数学内部定稿工作论文 · Zenodo

无交叉凸包分拆的秩计数与边点数不变性

将凸多边形边界上的有限个点分成若干块，要求不同块的凸包两两不相交。分拆的秩等于点数减去块数。本文计算每个秩上的分拆数量，并证明任意调换各边内部的点数都不改变这些数量。如果每条边都有内部点，各秩的数量还唯一确定各边点数及其重复次数。作为出发点的 Dougherty–Root 多边形构型非秩对称猜想及其互反恒等式，已由 Shivam Patel 证明；本文的新贡献是完整计数及任意边点数置换下的不变性。共线构型不在结论范围内。论文包含完整证明，尚未形式化。

Zenodo2026-09-09 代码与材料

2026-09-09

拓扑学内部定稿工作论文 · Zenodo

有向树上雪崩复形的普适实现

在并行筹码触发过程中，同时触发的顶点集合生成雪崩复形。本文从每个顶点初始仅有零或一粒筹码的构型出发，在朝向唯一吸收汇点的树上，将任意有顶点的有限单纯复形实现为雪崩复形的诱导子复形，并通过显式单纯塌缩去除辅助顶点、保留目标的同伦型。这解答了 Riihimäki–Smith 第 5 节问题 2 的有限球面楔和实现问题，以及随后提出的挠率与非楔和问题。相容回缩还可在细化时间并采样后实现非空有限滤过。另列的固定路径猜想 3.11 不在解答范围内。论文包含完整证明，尚未形式化。

Zenodo2026-09-09 代码与材料

2026-09-09修订 2026-09-10

组合数学内部定稿工作论文 · Zenodo

定权项链的逆余字典序通用循环

将仅相差循环旋转的单词归为一个项链。对长度与各位总和固定的非负整数单词，本文构造一个循环序列，使每个删去末位后的合法单词恰好出现一次。文章证明 Campbell–Janik-Jones–Sawada 猜想 8：按从末位开始比较的逆余字典序，连接各项链的最短重复块，所得循环正是原题指定的缺符号后继循环。生成每个符号的均摊时间为常数，辅助空间与单词长度成正比。证明还适用于在“将第一个正坐标的一单位移至下一坐标”操作下封闭的家族，包括对规范代表的前缀和施加限制的情形。论文包含完整数学证明，尚未形式化。

Zenodo2026-09-10 代码与材料

可信度与验证标准

形式化验证，是将定理和证明写成可由证明助手检查的精确形式。下面分别说明哪些检查已经完成、哪些前提仍然存在。

已完成内部审核的稿件（内部定稿）

内部定稿（Paper Close）表示该工作在公开前已完成整理和内部审核，并以工作论文形式发布。请将它作为普通学术预印本来阅读和讨论；后续检查或讨论仍可能带来更正。它不表示已经完成完整形式化或经过外部同行评审。

基于引用定理的机器验证（Reference-Gated）

代码以公开列明的引用定理陈述为输入，检查后续推导。引用定理本身的证明尚未纳入当前验证包；Reference-Gated 描述的是这一覆盖边界。

仅依赖基础公理的验证（Kernel-Only）

证明助手检查包括引用结果在内的全部定理依赖，不额外假设任何尚未证明的定理。只允许下列作为推理起点的基础公理。我们还检查形式化与论文的对应关系；文字表述仍可能需要修订。

propext (命题外延性); Classical.choice (经典选择公理); Quot.sound (商类型健全性).

同行评审 · 已录用

经过独立同行评审，获期刊或同行评审会议录用，代表外部学术认可；录用与正式发表分别记录。

我们唯一接受的最终形式化标准是 Kernel-Only。Reference-Gated 的信任程度较低，仅在工程规模特别大时作为中间版本发布。同行评审不能消除尚未证明的定理前提。

这些标准说明数学主张的证据状况。新颖性、归属及其与原问题的对应需要单独审查；公开后发现错误，应作更正或撤回。发布与纠错承诺

展开查看验证方法与适用边界

精确的定理依赖

引用结果必须有精确的定理陈述、来源及对应的已检查形式化定理。可以复用 Lean/mathlib 中已有的内核检查证明。所有依赖最终只能归结到 propext、Classical.choice、Quot.sound；不接受额外定理公理、sorry 或未经内核检查的原生计算捷径。

Reference-Gated 版本必须公开引用关口清单：精确命题、假设与量词、来源位置、形式化前提，以及依赖它们的结论。达到 Kernel-Only 必须用已检查证明消除每个关口，并重新检查最终定理及其与论文的对应关系。

最终定理的公理报告说明证明实际依赖什么。仍须核对其命题是否对应预期的数学定理；仅有公理报告不能确立这种对应。

我们认为，AI 辅助数学让明确的工程层愈发重要：将候选论证转化为经过检查、可读且可维护的成果。Proof Engine 研究纲领探索两种相互协作的角色：可靠地生产数学成果，以及解读成果、发展概念并开辟方向的结构研究。这两种角色可以重叠，AI 也可以参与其中；专业数学家在更深入的结构理解中仍发挥核心作用。公开问题是发展可复用数学贡献的起点。本纲领由实际成果、主张的证据、后续复用及纠错实践接受检验。详细论述见我们的研究纲领。

方法论