Improving Analytic Constants via Interpretable AI-Guided Lean Proof Refinement

Rahul Saha, Alan Li, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K. Kothari, Raghu Meka

* Equal contribution.

We develop a framework in which AI agents improve analytic bounds by refining individual lemmas within partially formalized Lean blueprints. The blueprint preserves the structure of the argument so that researchers can inspect each change, while Lean and certified numerical computations check the resulting bounds. We apply this approach to the Grothendieck and Korenblum constants, obtaining $K_G \le \pi/(2\log(1+\sqrt{2})) - 10^{-17}$ and $K_K \ge 0.356565$. Experiments examine how partial formalization and iterative refinement contribute to these improvements.

Read the paper · arXiv · Code