精读笔记

Problem Setting

《Optimizing Explicit Unit-Distance Lower-Bound Certificates》（arXiv preprint / 2026）实际处理的是 Sawin 显式 unit-distance 下界中的参数优化问题，而不是重新证明 Erdős 猜想的反例。给定 Sawin 已经建立的 sufficient criterion，任务是在有限数据 (T, SQ, k, R) 中找更好的 exponent gain δ。

真正困难点不是计算公式，而是可行域很不平滑：素数集合选择受 splitting/inertness 约束，GS inequality 给出硬预算，重数 k(p) 增加 numerator 的 log 收益但也放大 denominator，R 又在 numerator 的 log(1-1/R) 和 denominator 的 log(2R...) 之间形成 tradeoff。以前 Sawin 的显式参数更像 constructive witness，不是优化解；手工选择无法有效探索这个组合空间。

关键矛盾是：数学证明模板已经固定，理论自由度有限，但在 finite certificate 层面仍有大量可挖空间。本文把这个矛盾变成“在固定 theorem interface 下做离散优化”。

Motivation

已有路线的问题不是缺少一个可推出 n^{1+ε} 的证明框架，而是显式 ε 的数值被手工证书限制住了。Sawin 的工作把反例变成可量化 bound，同时也暴露出若干 finite parameters；这些参数没有理由是最优的。

作者的核心观察是：一旦证明系统给出一个可机械检查的 certificate criterion，提升常数就可以从数学推导问题转成 constrained search。这个缺口很明确：需要一个足够轻量、可复现、能处理数论 side conditions 的 optimizer/verifier pair，而不是再写一个不可审计的黑箱搜索。

所以本文动机更接近 computational mathematics：用 optimization 改进 explicit constants，并用 verifier 防止 heuristic search 变成不可验证猜测。

Core Idea

核心想法是把 Sawin criterion 中的选择自由度显式形式化为非线性整数规划。目标函数 δ=N/D 来自 Sawin 的 exponent formula；变量是有限素数集合 SQ、每个素数的整数 multiplicity k(p)、以及 rationally encoded R。约束则来自素数状态、admissibility 和 GS budget。

这种建模改变了问题的性质：原先是“找一个数学上好看的参数例子”，现在是“在硬约束 certificate space 中最大化一个可计算目标”。本质区别不在算法多先进，而在于证明参数被组织成 optimizer 可以反复评估的对象。

引入的 inductive bias 也很清楚：好的 certificate 应该用低 budget cost 的 prime 贡献尽可能多的 log(k+1) 收益，同时控制 denominator 中 prime powers 的增长。greedy 体现局部收益/成本偏好，integer ES 则允许跨变量协同调整。

Method

方法可以压缩成三个机制。

第一，certificate scoring。δ 的 numerator/denominator 直接作为 objective，所有候选都先按同一公式评分，再由 verifier 检查 side conditions。这解决的是 heuristic search 与数学有效性脱节的问题；优化器只负责提案，证明有效性由 deterministic checks 承担。

第二，budget-aware prime selection。GS inequality 被解释成资源约束，non-splitting prime 与 splitting prime 有不同成本。greedy 用单位成本收益排序来生成强 baseline。它需要存在，是因为从 Sawin 参数出发直接随机搜索效率低；greedy 提供了一个已经贴合目标函数结构的可行起点。

第三，integer-native evolutionary search。变量本身是 prime index、multipity、R numerator，而不是连续向量；所以用离散突变和 repair 比连续扰动后 round 更自然。repair 的作用不是优化，而是把搜索限制在 arithmetic feasible region 附近。两亲本离散重组带来的核心变化是允许组合不同候选的局部好结构，但文中证据显示其增益很小。

Key Insight / Why It Works

这篇论文有效的主要原因不是 evolution strategy 本身，而是 Sawin certificate landscape 存在可被简单搜索利用的 slack。Sawin published certificate 是一个显示性构造，不是经过系统优化的局部最优；因此只要把 objective 和 constraints 写清楚，greedy 就已经能吃掉一大部分增益。

最核心贡献是“把 explicit lower-bound certificate 转成可验证整数优化问题”。integer ES 是有用工具，但更像 test-time compute：在固定数学定理接口上花额外搜索预算找更优参数。它不是学习理论意义上的 generalization，也不是新 representation；更接近 constrained combinatorial search。

增益来源大致可归因如下：greedy 提升主要来自更合理的 SQ 替换和 multiplicity 重分配；ES 提升来自 coordinated changes，特别是把若干小素数/中等素数和 k(p) 调整到 denominator 惩罚与 numerator 收益的更好平衡；recombination 增益很小，可能只是搜索 stochasticity 和局部组合效应，不应过度解读。

哪些可能只是 engineering / scaling：候选素数上限、R grid/rational precision、population search budget、seeded initialization 都明显影响结果。当前没有消融能说明 Rudolph-style mutation 相比普通 local search、simulated annealing、tabu search 或 MILP/MINLP heuristic 有本质优势。换言之，算法标签不是关键，关键是有一个可快速评估且可 repair 的 certificate objective。

文中未充分说明 objective landscape 的结构，也没有给出局部最优性证明。因此 decimal improvement 应被看作“更好的已验证 witness”，不是“理解了最优证书结构”。

Relation To Prior Work

最接近的 prior 显然是 Sawin 的 explicit lower bound。本文没有替代 Sawin 的数论构造，而是站在其 criterion 之上优化参数。和 Sawin 的本质差异是：Sawin 提供 theorem + 一个 explicit witness；本文提供 search formulation + improved witness。

从技术谱系看，它属于 computer-assisted explicit constant optimization / certificate search，而不是 discrete geometry 的新 upper/lower bound 方法。与传统 combinatorial optimization 的关系也很直接：greedy knapsack intuition、integer evolutionary algorithm、repair operators 都是已有思想在数论 certificate 上的重组。

实质创新在于 problem packaging：把 class-field/Golod–Shafarevich 背后的 finite knobs 抽出来，形成可复现优化与验证流水线。看似新的 Tailored Integer Evolution Strategy，其实更多是已知 integer ES + domain-specific repair；真正新增的信息是这些启发式在 Sawin certificate space 中确实能找到更好参数。

Dataset / Evaluation

这里没有常规 dataset；evaluation 对象是一组 finite certificates。评估覆盖四类证书：Sawin baseline、greedy、integer ES、recombination ES。它验证的是 narrow claim：这些具体参数是否满足实现中的 arithmetic checks，并在公式 (1) 下给出更高 δ。

这个 evaluation 对核心 claim 的支持是部分充分的。若 claim 是“本文找到一个更好的 Sawin-style explicit certificate”，那么复现 Sawin baseline 加同 verifier 检查改进证书是合理证据。若 claim 是“方法系统性优化了该类证书”或“接近该路线可达上限”，证据明显不足：只有少量 runs、固定 T、有限候选池、没有强 baseline 对比、没有全局最优性或稳定性分析。

它也没有真实几何 realization。所有图示 lattice examples 都是解释性材料，不参与证书验证；certificate dashboard 也不是点集坐标。因此 evaluation 不验证 construction deployability，只验证 theorem-level parameter admissibility。

Limitation

最重要的前提是 Sawin explicit criterion 被完全正确引用，并且作者实现的 verifier 覆盖了所有必要 side conditions。作者也明确承认自己不是该数论方向专家；这使得独立验证尤其关键。

scalability 上限不清楚。当前搜索固定 T，候选素数 pmax=300，重数有界，R 在给定区间内 rationalized。δ 的提升可能只是当前有限窗口内的 engineering gain；扩大 T 或候选池后，搜索空间会迅速变复杂，repair heuristic 是否仍有效未知。

泛化也不应夸大。这里不存在跨任务泛化；只有在同一个 Sawin criterion 下搜索更好 witness。所谓“randomized optimization helps pure mathematics”是合理但宽泛的 statement，具体到本问题，增益主要来自更系统的 parameter sweep/search。

数值可靠性还有缺口。80-digit decimal margin 足以排除普通浮点误差，但 publication-grade certificate 应该用 formal interval arithmetic；Legendre/Kronecker 和 splitting checks 也最好由独立 Sage/Magma 重算。文中未充分说明这些 checks 是否完整等价于 Sawin 条件。

最后，没有 coordinate realization。论文把“存在性证书”与“显式点集坐标”区分得很清楚，但这也意味着结果仍停留在 asymptotic certificate 层面；从证书到可展示有限点集还需要一整套 computational number theory construction。

Takeaway

• 1. 这篇真正推动的是 explicit certificate optimization 的工作流：把数学证明中的自由参数显式暴露为可搜索对象，并用 verifier 把 heuristic 和 theorem validity 分离。
• 2. 对这类问题，最大收益往往不是发明复杂优化器，而是找到正确的 certificate parameterization、正确的可行域 repair、以及足够便宜的 objective evaluation。
• 3. Sawin-style 下界目前远未被参数优化耗尽；固定 T 的小规模搜索已经能提升 δ，说明更系统的 T-search、branch-and-bound、hybrid local search 或 formal verified optimization 可能还有空间。
• 4. 可迁移 insight：许多纯数学 explicit constants 可以被看成 constrained witness search；关键是让 witness format 可机械验证，而不是让 heuristic 本身可信。

一句话总结

这篇论文不是新的 unit-distance 证明，而是把 Sawin 显式下界中的有限证书选择转化为可复现的整数优化与验证问题，并用轻量 heuristic search 给出一个更好的 Sawin-style exponent witness。