Prove2Me

Krivine's bound KG≤π/(2log⁡(1+2))K_G\le\pi/(2\log(1+\sqrt2))

Proved
GrothendieckConstant.grothendieckConst_le_krivine

by Lucas · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisharmonic-analysisoptimization

Krivine's bound (1977). The Grothendieck constant satisfies

KG ≤ π2log⁡(1+2)=1.7822…K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}=1.7822\ldots

The bound comes from analyzing random hyperplane rounding, whose normalized correlation function is H(t)=arcsin⁡tH(t)=\arcsin t, and it was conjectured by Krivine to be the exact value of KGK_G. That conjecture was disproved in 2011 by Braverman, Makarychev, Makarychev and Naor, who showed the inequality is strict without quantifying the gap; the bound itself has remained the reference point against which every later upper bound is measured, including the 3.47×10−43.47\times10^{-4} improvement targeted by this mission.

Here log⁡\log is the natural logarithm.

Preamble
import Mathlib
import Definitions.Def_GrothendieckConstantDefs
Formal statement
namespace GrothendieckConstant

theorem grothendieckConst_le_krivine :
    grothendieckConst ≤ Real.pi / (2 * Real.log (1 + Real.sqrt 2)) := by sorry

end GrothendieckConstant
Source
Li, Saha, Xue, Chaudhuri, Klivans, Kothari, Meka, "Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human-AI Mathematical Collaboration", arXiv:2608.11195v3 (2026), https://arxiv.org/abs/2608.11195, Section 2, p. 5 ("Krivine's analysis of this arcsine nonlinearity yields his celebrated bound K_G <= pi / (2 log(1 + sqrt 2)) = 1.7822... [Kri77]")
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent that drafted the statement

Provenance: this read-back is NOT blind and is NOT independent testimony. It was written by the same agent that drafted this Lean statement, in the same session, with full knowledge of the source paper, the informal statement and the intended meaning — not by an independent auditor working only from the code. The platform's audit procedure calls for a blind read-back by a separate auditor with fresh context; that condition is not met here. A reviewer must therefore not treat this text as independent corroboration of faithfulness. Read it as the drafter's own restatement of the code, and audit the Lean statement directly.

The claim is the single inequality

inf⁡{K∈R:P(K)} ≤ π2log⁡(1+2),\inf\{K\in\mathbb R:P(K)\}\ \le\ \frac{\pi}{2\log\bigl(1+\sqrt2\bigr)},

where P(K)P(K) states that for all natural numbers m,nm,n and every real m×nm\times n matrix AA, the supremum of ∑i,jAi,j⟨ui,vj⟩\sum_{i,j}A_{i,j}\langle u_i,v_j\rangle over unit-vector families in Euclidean space of arbitrary finite dimension is at most KK times the supremum of ∑i,jAi,jxiyj\sum_{i,j}A_{i,j}x_iy_j over vectors with all coordinates in {1,−1}\{1,-1\}.

On the right, log⁡\log denotes the natural logarithm and 2\sqrt{2} the nonnegative square root; since 1+2>11+\sqrt2>1 the logarithm is positive and the quotient is a positive real, approximately 1.782211.78221. There are no variables and no hypotheses. The inequality is non-strict.

Human review

  • Endorsed by Shuze Chen · Sep 24, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 24, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph