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

Zenodo2026-09-06

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

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

占位有界筹码图中的匹配与独立数

构型把固定数量的不可区分筹码放在图的顶点上，每步沿一条边移动一个筹码。在不限占位数或采用统一偶数占位上限时，若二部底图有一组端点不交的边覆盖某一侧的全部顶点，则该侧占位总数为偶数的构型组成最大独立集：它们之间没有一步合法移动，也不存在更大的、具有这一性质的构型集合。这证明了超筹码图独立数猜想。论文还给出不同顶点容量下的充分条件，以及奇数容量的显式反例。

Zenodo2026-09-06

2026-09-07

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

稳定连续模式与链簇

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

Zenodo2026-09-07

2026-09-07

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

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

Zenodo2026-09-07

2026-09-07

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

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

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

Zenodo2026-09-07

2026-09-07

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

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

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

Zenodo2026-09-07

可信度与验证标准

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

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

已完成内部审核并公开，主要结论的完整形式化尚未确立；仍可能存在错误。

有外部定理前提的验证（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 时代数学的重要变化不只是成果数量的增长，更在于快速生成的内容凸显了既有数学体系中验证、解读、复用与维护之间缺失的工程层，并推动新的研究分工。AI 可以参与生成候选论证和探索证明路径，数学工程师等新兴角色将这些内容组织为可检查、可复现、可持续使用的成果，而数学家在提出有价值的问题、发现结构、创造概念以及解释和推广结果方面发挥核心作用。这些角色可以相互重叠，Proof Engine 正通过公开数学案例探索这种分工的基本可行性。详细论证见我们的方法论论文。

方法论