Building the Mine, Not the Miner: How AI Helped Tighten the Grothendieck Constant

Paper: 2608.11195 Authors: Alan Li, Rahul Saha, Anton Xue, Swarat Chaudhuri, Adam Klivans, Pravesh K Kothari, Raghu Meka Categories: cs.AI, cs.CC, cs.HC, math.FA

The Gap

Two literatures are stuck in different ways, and this paper wedges them together.

On the math side: the Grothendieck constant $K_G$ is the exact price you pay for relaxing a $\pm 1$ optimization problem into a vector-valued one. Its value has been famously unresolved since 1953. The upper bound $\pi/(2\log(1+\sqrt\{2\})) \approx 1.78221$ is Krivine’s from 1977, and Krivine conjectured it was the truth. Braverman–Makarychev–Makarychev–Naor (2011) proved it is not the truth — but their improvement was an unspecified $\varepsilon$, a non-constructive “strictly less than.” On the other side, the best lower bound has sat at Davie’s and Reeds’ $\approx 1.67696$ since the mid-1980s. So the state of the art was roughly: $K_G \in [1.67696,\ 1.78221)$, with one endpoint known to be loose by an amount nobody could name.

On the AI side: we have plenty of demonstrations that models can do competition math, and plenty of formalization efforts in Lean, and a growing pile of “an AI helped with a lemma” anecdotes. What we don’t have is a usable account of workflow — what does a human do to make an agent productive on a problem where nobody knows the answer, where there is no benchmark label, and where the reward signal arrives weeks later? The abstract’s own framing is blunt about this: agents are “increasingly used,” but “it is often unclear how to use them effectively.”

[ Gap ] AI helps with math sometimes, but nobody can say HOW
        (and K_G has been stuck for ~40 years)
   |
   +-- assumption: research progress here == search over a
   |               parametrized space that has a CHEAP, SOUND
   |               correctness signal
   v
[ Method ] humans carve the space and build the oracle
           AI runs the long-horizon search inside it
           humans prune, verify, and write the proof
   |
   v
[ Evidence ] two hard numbers, not vibes:
             6*pi/11  <=  K_G  <=  pi/(2 log(1+sqrt2)) - 10^-4
             i.e. [1.71360, 1.78211]  vs old [1.67696, 1.78221)
   |
   v
[ Conclusion ] AI can reach insights experts call novel
               *conditional on* the problem being pre-digested
               into a searchable form

The Increment

One sentence: Before, “AI contributed to a real math result” was a claim you had to take on faith and a 40-year-old constant had a 0.105-wide window; after, the window is 0.069 wide, one endpoint of the old window is quantitatively refuted, and there’s a written protocol for how the collaboration was set up.

Core Mechanism

The mechanism is a division of labor, and the paper’s real content is where the line gets drawn. Humans do the outer loop: pick a problem whose difficulty is concentrated in a search rather than in a conceptual leap, then reduce it to a parametrized family — a family of matrices for the lower bound, a family of rounding schemes for the upper bound — and expose an evaluation function that says “this candidate scores $x$.” The AI system does the inner loop: propose candidates, run the symbolic and numerical machinery (SDP solves, integral evaluations, series expansions), notice patterns, and iterate for far longer than a human would tolerate.

For the lower bound, the shape of the answer is a tell. $6\pi/11$ is exactly $(12/11)\cdot(\pi/2)$, and $\pi/2$ is Grothendieck’s original lower bound coming from the Gaussian/arcsine identity. A clean rational multiple of $\pi$ almost always means a small finite gadget was found and then analyzed in closed form, rather than a numerical optimum reported to six digits. That is precisely the kind of thing a tireless search plus a human who recognizes “wait, that decimal is $6\pi/11$” produces together: the machine finds the configuration, the human names it, and then the closed form makes the proof writable.

For the upper bound, the work is the opposite flavor: not discovery but epsilon-chasing. BMMN already knew Krivine’s scheme is suboptimal; turning that into $-10^\{-4\}$ means carefully tracking a perturbation of the rounding function through a pile of integrals and inequalities with every constant made explicit. This is bookkeeping that humans reliably decline to do, and where a system that never gets bored and can re-derive each step numerically as a sanity check has a genuine comparative advantage.

   HUMAN (outer loop)                 AI SYSTEM (inner loop)
  ...........................        ..............................
  : choose K_G, both bounds  :       : recall/rederive prior work  :
  : decide what is worth     :       : symbolic algebra, integrals :
  :   attacking              :       : numeric SDP / optimization  :
  :                          :--spec>: candidate generation        :
  : reduce to parametrized   :       : long-horizon iteration      :
  :   family + objective     :       : self-check against oracle   :
  :                          <-cand--:.............................:
  : prune, spot closed form  :                    |
  : write and verify proof   :          fast oracle: does this
  :..........................:          candidate beat the record?
             |                                    ^
             |                                    |
             +---- humans BUILD this oracle ------+
             v
      theorem + case study writeup

Structural metaphor: this is mining, not exploration. A geologist reads the terrain and says “there is a seam under this ridge, sink the shaft here” — that is the human choosing $K_G$ and reducing it to a specific parametrized family. The drilling rig runs day and night and does not care that it is boring — that is the agent’s long-horizon iteration. The assay lab tells you within minutes whether what came up is ore or pyrite — that is the cheap numerical oracle, and the whole operation collapses without it, because a rig with no assay lab just makes a very large pile of rock. The smelter that turns ore into a certified bar is the human-written proof: nothing counts until it passes that step. And the failure mode is the one you’d expect from a rig: it will happily drill a beautiful hole through granite forever, because deciding *where to drill was never its job.

Key Concepts

• The Grothendieck constant, i.e. the price of relaxation: Take any matrix $A$. First, maximize $\sum`_{i,j}` A_{ij} x_i y_j$ over signs $x_i, y_j \in \{-1,1\}$ — a combinatorial problem, generally NP-hard, this is essentially the $\infty \to 1$ norm. Now cheat: replace each sign by a unit *vector and each product $x_i y_j$ by an inner product $\langle u_i, v_j\rangle$. Suddenly it’s a semidefinite program you can solve in polynomial time, and the value only went up. $K_G$ is the worst-case ratio between the two, over all matrices. It is the exact integrality gap of that SDP. Concretely: if your SDP says 178, the true sign-value could be as low as 100, but never lower. Physicists know the same number from another door — by Tsirelson’s work it governs the maximum quantum-over-classical advantage in two-player XOR games, so the ”$\pm 1$ vs. vectors” gap is literally the classical-vs-quantum gap for Bell-type experiments.
• Why Krivine’s bound looks the way it does: If you take two unit vectors at angle with inner product $\rho$ and round them with a random hyperplane, the expected product of the resulting signs is $\frac\{2\}\{\pi\}\arcsin\rho$ — Grothendieck’s identity. That $\arcsin$ is a distortion you don’t want. So pre-distort: apply a function $f$ to the vectors first such that $\arcsin(f(\rho))$ comes out proportional to $\rho$. The inverse of $\sin$-composed-with-what-you-want is $\sinh^\{-1\}$, and $\sinh^\{-1\}(1) = \log(1+\sqrt\{2\})$ — which is where $\pi/(2\log(1+\sqrt\{2\}))$ comes from. Once you see this, you also see the weakness: the scheme is tuned to be tight at $\rho = \pm 1$ and it’s one single scalar function applied uniformly. Beating it means giving up that elegance, which is exactly the sort of ugly, high-dimensional search a machine can do and a human resents.
• The well-posedness tax: The hidden cost in any “AI did research” story. An agent can only search a space you have described, scored by a signal you have implemented. Converting “improve the lower bound on $K_G$” into “search matrices of this form, score by this ratio, reject anything the SDP solver won’t certify” is human intellectual work that happens *before the impressive part, and it’s usually invisible in the write-up. The most useful thing this paper can do is make that step visible.

Framework Shift

Before (mainstream approach):          After (this paper):

  [ human ]                              [ human: outer loop ]
     |  "prove this theorem"              choose problem
     v                                    carve search space
  [  LLM  ]  ----> proof attempt          build cheap oracle
     |                                       |         ^
     v                                       | spec    | ore
  [ human reads it, sighs ]                  v         |
                                        [ AI: inner loop ]
  scored on: benchmarks with              generate + test
  known answers                           for weeks, no boredom
  credit: unfalsifiable                      |
                                             v
                                        [ human: verify, name
                                          the closed form, prove ]

                                        scored on: an OPEN problem's
                                        record. either the number
                                        moved or it did not.

One sentence: from asking a model to be a mathematician to building an environment in which search is cheap and letting the model be a drilling rig, the core shift is that the human’s job moves from prompting to problem reduction and oracle design.

Expert Assessment

Problem choice: Real gap, and shrewdly chosen on both axes. $K_G$ is a genuinely famous stuck constant where the remaining difficulty is unusually search-shaped — you are hunting configurations and rounding functions, not inventing a new cohomology. That makes it close to the best available testbed for this claim, which is also the honest caveat: the result tells you what agents can do on problems of this *type, and the paper should not be read as evidence about conceptual mathematics. The AI-workflow literature genuinely lacks documented, verifiable end-to-end cases, so the case-study framing fills a real hole rather than a manufactured one.

Method maturity: The system is scaffolding, not science. Long-horizon loop, tool use, self-checking against a numerical oracle — nothing here is an architectural contribution, and readers hoping for a new agent design will be disappointed. The cleverness is entirely in the reduction and in the choice of which two sub-tasks to hand over: closed-form-shaped search for the lower bound, explicit epsilon-chasing for the upper bound. That’s a good instinct, and I’d argue it’s the transferable part. Simpler approach being overlooked? Possibly: a well-tuned classical search (branch-and-bound plus an SDP solver plus a human) might have found $6\pi/11$ too, and the paper cannot rule that out.

Experimental integrity: The math is the saving grace — $6\pi/11$ and $-10^\{-4\}$ are checkable by third parties, which is a much stronger anchor than any benchmark table. Everything about the *AI claim, though, is $n = 1$ with no control condition and no ablation. How much of the credit belongs to the agent versus the humans who carved the space is fundamentally unfalsifiable here, and “insights deemed novel by domain experts” is doing a lot of work in the abstract when the domain experts are co-authors. I’d also want to know the denominator: how many problems did this team attack this way, and how many produced nothing? Publishing only the one that worked is a selection effect the paper should name out loud.

Writing quality: The likely corner-cut is the case study itself, which is the part with no formal standard to hold it up. Qualitative “strengths and weaknesses” narrative is the easiest section to write vaguely and the hardest to learn from. The rewrite that would elevate the whole paper: a chronological decision log with the dead ends included — dates, what was tried, what the agent proposed that was wrong and *how it was wrong, how many candidate families were rejected before the good one, and which specific human interventions unblocked things. The failures are the data. Without them this is a well-earned trophy with an anecdote attached.

Verdict: weak accept — the mathematical result is solid and independently checkable, and the workflow framing is genuinely needed, but as an empirical claim about AI-for-research it’s a single uncontrolled case whose most valuable evidence (the process log) is the part most likely to be thin.

Takeaways

Concrete things to steal:

• Split the loop by boredom tolerance. Give the agent tasks where the difficulty is volume and patience, not taste. Two archetypes appear here and both generalize: (a) sweep a parametrized family against a scoring function; (b) take an existing non-constructive “strictly better than X” result and grind out an explicit constant. Type (b) is a criminally underexploited niche — there are hundreds of theorems in the literature with an unspecified $\varepsilon$ that nobody wants to make explicit.
• The oracle is the deliverable. Before prompting anything, ask: can I score a candidate cheaply and soundly? If the answer is no, you don’t have an agent problem yet, you have a formalization problem. Budget your own time for building the assay lab, not for prompt engineering.
• Numeric-to-closed-form as an explicit pipeline step. Machine finds $1.7136...$; human (or a table lookup / inverse symbolic calculator) recognizes $6\pi/11$; the closed form is what makes a proof writable and a result publishable. Wire this step in deliberately instead of hoping someone squints at the right decimal.
• Don’t let the agent grade its own novelty. “Is this new?” is a literature question with an adversarial failure mode. Route it to a search over prior work and a human who knows the field, and treat agent-reported novelty as a hypothesis.
• Keep the decision log from day one. Whether or not this paper’s log is thorough, yours should be — it’s the only artifact that lets anyone, including future you, distinguish “the agent did it” from “the setup did it.”

What not to take: any belief about how well this generalizes to problems where the hard step is deciding what to search for. That question is untouched here, and the paper’s own framing — “creating ideal conditions” — quietly concedes it.