AI tightens mathematical proofs by working on their weakest estimates

Improve the estimate, preserve the argument

A mathematical proof can establish a correct bound without establishing the best possible one. Intermediate steps often use convenient estimates that sacrifice precision. Tightening those steps can improve the final result without changing the proof’s central idea.

In an arXiv preprint, Rahul Saha and colleagues investigate whether AI agents can systematically find such opportunities. Their demonstrations concern Grothendieck’s constant, which connects discrete optimization with continuous approximations, and Korenblum’s constant, which concerns comparisons between complex functions. These are mathematical results supported by computational proof refinement, not physical experiments.

The important qualification comes early: the paper itself acknowledges stronger bounds obtained by other work. Its headline numbers should therefore be understood as improvements within particular historical proof approaches, not as current world records.

A blueprint with editable estimates

The researchers first organize an existing argument into a dependency graph: definitions and intermediate results feed into later deductions and ultimately the target theorem. Humans choose the proof structure and identify quantities the agents may improve.

Parts of this blueprint are expressed in Lean, a proof assistant that checks whether deductions follow from their stated premises. Other background mathematics remains explicitly assumed. Numerical inequalities are checked separately using Arb, an interval-arithmetic library that encloses numerical answers within rigorous bounds rather than merely calculating approximate decimal values.

Three agent roles divide the work. A planner identifies a promising refinement and specifies its obligations. A generator edits the proof and numerical machinery. An evaluator checks the candidate against the permitted assumptions, recomputes numerical bounds and decides whether the result improves.

Keeping the main dependencies fixed gives researchers a way to inspect what changed and how that change affects the conclusion. It does not mean every underlying mathematical fact has been formally proved from scratch.

Tiny final changes can require substantial mathematics

For the real Grothendieck constant, the framework builds on an existing argument showing that Krivine’s classical upper bound, approximately 1.78221, is not optimal. Earlier work established a positive gap without specifying its size. The researchers report an explicit subtraction of ten to the minus seventeen from Krivine’s expression.

That is an extraordinarily small change to the bound itself. The paper’s much larger improvement factors concern the size of the certified subtraction or intermediate error estimates—not a comparable reduction in Grothendieck’s constant.

One successful strategy replaces separately bounded factors with a bound on their combined expression. Separate worst-case estimates can exaggerate an error because the factors need not reach their worst values together. Exact derivative identities also expose cancellations that coarse estimates conceal. The reported final intermediate remainder constant falls from roughly eight hundred trillion to two sevenths.

For Korenblum’s constant, the question is how much of the outer region of a unit disk must be inspected to guarantee a comparison of two functions’ total squared magnitudes. A larger admissible inner radius means a thinner outer region suffices.

The main run raises Wang’s 2025 lower bound from 0.3554 to 0.356565, an absolute increase of 0.001165. Its key refinement retains information about individual terms in a coefficient expansion instead of combining them prematurely into a looser estimate. Neither case determines the constant’s exact value. A footnote reports stronger bounds elsewhere: a Grothendieck upper bound of 1.7799 and a Korenblum lower bound of 0.4263.

What the checks do—and do not—establish

The most revealing limitation is a numerical error discovered during the project. Early Grothendieck calculations evaluated a truncated series without rigorously bounding the omitted tail. Interval arithmetic could enclose the truncated calculation correctly while still failing to bound the intended function.

The researchers report a human-directed audit and repair outside the agent loop, followed by revised candidates using truncation-free calculations. The final result uses this repaired approach. However, the Grothendieck comparison experiments retain the earlier evaluator; their numerical scores measure search performance under that evaluator, not independently certified mathematical improvements.

Those comparisons favor the full framework over simplified workflows, but each configuration has only one run. They do not establish general performance across mathematics. The released final Grothendieck record also lacks two numerical certificate caches, which must be regenerated to rerun that checking stage.

The contribution is consequently narrower than autonomous theorem discovery: expert-designed structure helps agents improve local mathematics. Lean checks deductions from assumptions; external numerical code and the correspondence between its calculations and those assumptions remain essential parts of the trust boundary.