一句话总结

本文利用 MechMath Agent Team 自动生成自然语言证明及其 Lean 4 形式化证明，证明了每个非负整数均可表示为一个三角形数、一个五边形数与一个七边形数之和，从而解决了 OEIS A287616 猜想。

核心贡献

• 本文证明了对于任意自然数 $x, y, z$x,y,z，每个非负整数均可表示为 $x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2$x(x+1)/2+y(3y+1)/2+z(5z+1)/2，从而解决了 OEIS A287616 猜想。
• MechMath Agent Team 框架自动生成了该结果的完整自然语言证明及其对应的 Lean 4 形式化证明。
• 生成的 Lean 4 形式化证明覆盖了完整的推导过程，仅有一处外部引用的定理和一项符号计算验证尚未形式化。

引言

数论长期致力于研究整数如何分解为多边形数等特定序列的和，这一基础性探索不仅强化了加性组合数学，也为整数表示的算法方法提供了指导。早期研究已成功证明每个非负整数均可表示为三个三角形数之和，但将这些结果推广至混合多边形数族需要繁琐的分情况讨论，且留下了大量组合未经验证。作者通过系统的代数化简与针对性的计算验证，证明了每个非负整数均可表示为恰好一个三角形数、一个五边形数与一个七边形数之和。该成果填补了广义多边形数定理中的特定空白，并为未来的加性数论研究明确了路径。

数据集

• 数据集构成与来源： 作者提供了一个公开可访问的代码仓库，作为该项目的完整数据归档。其中包含完整的 Lean 4 源代码、构建说明，以及为有限覆盖证明生成的精确计算机证书。
• 子集划分： 仓库被划分为两个独立的软件包。formalization/ 软件包包含 Lean 开发文件，基于 Mathlib v4.29.0 进行构建。verification/ 软件包保存了精确的双层覆盖结构、各单元证书以及独立验证器。
• 使用与组织方式： 作者利用该仓库确保研究具备完全的可复现性与透明度。详细的 README 文件将数学证明的每个组成部分直接映射至对应的 Lean 形式化证明或证书工件，为读者建立了清晰的参考路径。
• 处理与验证细节： 项目采用 Lake 项目结构进行依赖管理与形式化开发。验证工作流使用自定义验证器处理各单元证书，以独立方式重新推导证明结论，确保每个数学步骤均有机器可验证的证据支持。

方法

作者采用了一种化简策略，将原始表示问题转化为带约束的三元二次型问题。通过应用基础平方恒等式，目标方程被映射为 $Q(u, v, w) = 15u^2 + 5v^2 + 3w^2$Q(u,v,w)=15u2+5v2+3w2，其目标在于寻找满足特定奇偶性与同余条件的整数坐标。该变换将计算重心转移至构造原始表示，并通过结构化的下降过程对其进行系统优化。

该框架首先为任意有效输入确立原始种子。作者运用 $p$p-adic Hensel 提升法验证所有素数模下的局部表示性。随后应用基于类域的局部-全局原理，保证该二次型或其类域伴生元能够原始表示目标整数。有理转移机制将类域伴生表示映射回原始形式，为后续的下降阶段提供有效的原始起点。

获得原始表示后，作者实现了一种由字典序势函数引导的有限下降过程。该下降过程基于一组保持二次型不变并维持坐标原始性的有理相似变换。每次变换均通过调整坐标的奇偶性与剩余类，严格降低势函数。作者定义了五条基础单步下降规则，覆盖了绝大部分搜索空间，通过符号提升与模运算调整将状态导向目标同余条件。

基础下降规则会留下一个狭窄的残差区域，其中标准操作无法立即满足所需条件。为解决这一空白，作者将残差空间划分为有限个符号-剩余单元。他们证明，任何短下降词的成功仅取决于有界的符号评估与模剩余集合。这种确定性将无限下降问题转化为有限验证任务。随后，作者构建了一个精确的有理线性规划覆盖，用于枚举残差锥内所有可实现子单元。每个子单元均通过显式整数见证与有界长度的逃逸词进行认证，确保下降过程在不依赖浮点运算或采样的前提下终止于有效状态。

全部数学核心逻辑均被编码至证明辅助框架中。作者形式化了平方化简、原始种子构造、传输恒等式、基础下降演算以及残差空白分析。该形式化过程隔离了两个外部输入：经典类局部-全局定理与有限线性规划覆盖证书。所有逻辑依赖均经过内核检查，确保下降算法与最终表示定理均通过机器验证。

实验

实验评估了针对与残差锥相交的符号锥所采用的双层覆盖策略，验证了不同长度的代数词是否能够有效认证不同几何区域内的符号行为。分析表明，几乎所有锥体均能通过深度为三的单词成功验证，而少数上界锥则需要长度为四的单词以及对极射线的显式几何验证。这种分层方法有效地限制了新形式的符号变化范围，证明了将针对性词长与精确有理锥检查相结合，能够可靠地捕捉排列过程中的符号变化。

作者对双层覆盖结构进行了计算分析，指出大多数符号锥可通过深度为三的单词解决，仅有少数需要长度为四的单词。实验量化了该验证过程的复杂性，表明该过程生成的更近拉回发射量显著多于精确行状态量。扩展后的排列结构包含大量相对于原始集合的新形式。更近拉回发射量的体积远超精确行状态的数量。新形式集合在并集的总形式中占据主要部分。实验区分了不同的坐标读取形式与拉回更近形式。

作者分析了涉及符号锥与上界锥的双层覆盖结构，指出多数锥体较为简单，而少数子集需要复杂证书。实验通过追踪精确行状态、发射量及各类形式量化了结构复杂性。结果表明，更近拉回发射量显著多于精确行状态，且拉回更近形式的数量多于坐标读取形式。分析区分了简单符号锥与复杂上界锥，后者需要精确的有理锥成员资格检查。数据显示，更近拉回发射量的体积明显大于精确行状态。不同拉回更近形式的数量显著高于不同坐标读取形式的数量。

该计算分析评估了双层覆盖结构，以衡量符号锥与上界锥的验证复杂性与结构扩展情况。实验表明，尽管多数锥体结构简单且可通过极小深度解决，但少数子集需要更复杂的有理成员资格检查。定性来看，与精确行状态和坐标读取形式相比，验证过程产生了显著更多的更近拉回发射量与拉回形式，这表明扩展排列结构大幅拓宽了整体形式空间。