智能体在Lean蓝图里只收紧局部引理，Grothendieck常数上界首次得到显式数值改进
核心概要
AI智能体不再重写整份证明，而是在人类搭好的Lean蓝图里逐条收紧中间估计，让局部改进沿依赖图自动传到最终界。对Grothendieck常数，这一流程给出Krivine 1977年上界之后的首次显式数值改进；对Korenblum常数，它改进了Wang 2025年的下界。把蓝图去掉后，智能体写了大量Lean代码却没有任何改进。
深度剖析
解析常数的上界或下界可以只靠收紧证明中某几条中间引理来改进，而不必重建整个论证。 此前的AI数学系统多从问题陈述出发生成新证明，产出的论证对人类难以检查和理解；而现有证明的中间引理往往留有松弛，这些松弛此前没有被系统性地定位和收紧。 在Grothendieck常数上，收紧Braverman等人证明中Lemma 5.4的余项常数后，得到Krivine 1977年上界之后的首次显式数值改进；在Korenblum常数上，下界在Wang 2025年结果的基础上得到提高。
证明被写成部分形式化的Lean蓝图，即定义、引理与定理组成的依赖图，每段Lean代码对应图上一个节点。 智能体在保持依赖图不变的前提下迭代修改Lean代码，可以引入辅助引理、发现新恒等式或优化中间参数，改进沿图自动传播到最终界。 规划器、生成器、评估器三个角色分工运行；符号推导由Lean检查，数值估计由Arb区间算术库出具证书，评估器只在两道检查都通过时接受修改。
去掉蓝图后改进完全消失，说明可编辑的中间命题是这套流程起作用的关键。 在匹配计算预算的消融中，保留完整智能体系统但只把已发表界作为公理的配置没有任何改进。 该配置在Korenblum上写了大量Lean代码且评估器全部通过，但没有可收紧的中间命题，预算都花在重建证明结构上。
启示与展望
演示范围限于两个解析常数：Grothendieck常数的上界与Korenblum常数的下界，且每个问题的蓝图、可编辑节点和认证方式都由作者事先确定。作者指出，同一结构原则上可支持证明压缩、更快的证书、更少假设和更简洁的依赖，但这些只是讨论中的可能扩展，未在实验中实现。
作者说明，每个新问题都要人工决定哪些证明成分可编辑、什么算有效改进、候选如何认证，因此搭建环节依赖专业知识。Grothendieck常数与Korenblum常数的界在投稿后都已被其他工作更新，文中数值应放在当时的比较背景下看。