Optimizing Analytic Constants via AI-Guided Lean Proof Refinement

We demonstrate that AI agents can autonomously improve mathematical proofs of quantitative results. As a key step towards this frontier, we achieve strict improvements on Grothendieck's and Korenblum's constants, whose precise values have remained surprisingly elusive despite their recurrence in both the mathematical and physical sciences. By encoding relevant literature as a partially formalized Lean blueprint, we structure the agent's search space to localized proof refinements that automatically propagate to a verified final bound. Concretely, Grothendieck's constant ($\mathcal{K}_G$) is shown to be: $$ \mathcal{K}_G \leq \tfrac{\pi}{2 \log (1 + \sqrt{2})} - 10^{-17}, $$ which is the first explicit numerical improvement since Krivine's landmark 1979 result. For Korenblum's constant ($\mathcal{K}_K$), the lower bound is tightened to: $$ \mathcal{K}_K \geq 0.3554 + 0.001165, $$ a third-digit improvement over Wang's recent 2025 result. In summary, we establish that AI agents can autonomously refine formal proofs of open problems and provide a generalizable framework for future mathematical discovery.