Agents tighten single lemmas inside Lean blueprints, giving the first explicit numerical improvement on Grothendieck's constant upper bound

A bound on an analytic constant can be improved by tightening a few intermediate lemmas in an existing proof, without rebuilding the whole argument. Earlier AI mathematics systems mostly generated new proofs from a problem statement, producing arguments that humans found hard to inspect and understand; existing proofs often contain slack in intermediate lemmas, and that slack had not been located and tightened systematically. On Grothendieck's constant, tightening the remainder constant in Lemma 5.4 of the Braverman et al. proof yields the first explicit numerical improvement over Krivine's 1977 upper bound; on Korenblum's constant, the lower bound is raised above Wang's 2025 result.

The proof is written as a partially formalized Lean blueprint, a dependency graph of definitions, lemmas and theorems, with Lean code attached to each node. The agent iteratively edits the Lean code while keeping the dependency graph fixed, and may introduce auxiliary lemmas, discover new identities or optimize intermediate parameters, so improvements propagate automatically to the final bound. A planner, a generator and an evaluator split the work; Lean checks the symbolic deductions, the Arb interval-arithmetic library certifies the numerical estimates, and the evaluator accepts an edit only when both checks pass.

Removing the blueprint erases the improvement entirely, indicating that editable intermediate claims are what make the pipeline work. In a budget-matched ablation, a configuration that kept the full agentic system but reduced the published bound to an axiom produced no improvement. That configuration wrote plenty of Lean on Korenblum and passed every evaluator run, but had no intermediate claim to sharpen and spent its budget trying to rebuild the proof structure.

The demonstrated scope is two analytic constants: an upper bound on Grothendieck's constant and a lower bound on Korenblum's constant, with the blueprint, editable nodes and certification scheme fixed by the authors for each problem. The authors note that the same structure could in principle support proof compression, faster certificates, fewer assumptions and cleaner dependencies, but these are discussed as possible extensions and are not implemented in the experiments.

The authors state that each new problem requires deciding by hand which proof components are editable, what counts as a valid refinement and how candidates are certified, so setup depends on expertise. The bounds on Grothendieck's constant and Korenblum's constant have both moved since submission, so the reported numbers should be read against that comparison context.