Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human-AI Mathematical Collaboration

This paper presents an extensive case study of a long-horizon human–AI mathematical collaboration aimed at improving bounds on the Grothendieck constant K G, which captures the hardness between combinatorial problems and their continuous relaxations. The collaboration tightened the best known bounds to:

[

6 pi over 11 = 1.7135 K G pi over 2 (1+ sqrt 2) - 3.47 times 10-4 = 1.7818

]

The upper bound comes from a new asymptotic framework for rounding algorithms, and the lower bound from the first argument that bounds K G from below without constructing a hard instance. Central steps of this mathematics originated with the AI system and were judged novel by domain experts; all results stated as theorems have been independently verified by the authors, with complete proofs appearing in a companion paper [SLX+ 26].

The paper explains the mathematical problem. Given a matrix A = (a ij) in R m times n, one seeks sign vectors maximizing the bilinear form OPT(A):= x in plus or minus1 m, y in plus or minus1 n sum i,j a ij x i y j. This is NP-hard in general. A standard relaxation replaces each sign with a unit vector and each product with an inner product: SDP(A):= u i, v j in S d-1 sum i,j a ij u i, v j, which is solvable in polynomial time. Since every sign is a one-dimensional unit vector, OPT(A) SDP(A). Grothendieck's inequality guarantees a universal constant K such that SDP(A) K times OPT(A) for every matrix A. The Grothendieck constant K G is the smallest such K, representing the worst-case integrality gap of the canonical SDP relaxation.

The paper describes rounding schemes as partitions: A Krivine scheme is a pair of partitions of R k into a +1 region and a −1 region, encoded by odd sign functions f, g: R k to plus or minus1. The algorithm maps each SDP vector to a random Gaussian point in R k, arranged so points of u i and v j are correlated according to u i, v j, then labels each vector by the region its point lands in. The normalized correlation function is H(t):= pi over 2 E[f(X)g(Y)], where X, Y are standard Gaussian points with pairwise coordinate correlation t. For the half-space partition, Grothendieck's identity gives H(t) = t, and Krivine's analysis yields his celebrated bound K G pi over 2 (1+ sqrt 2) = 1.7822

Krivine conjectured this value optimal, but Braverman, Makarychev, Makarychev, and Naor disproved it in 2011 by mixing hyperplane rounding with a carefully chosen two-dimensional scheme, establishing the strict inequality without quantifying the gap [BMMN11]. Naor and Regev later proved a striking converse: such mixed Krivine schemes are asymptotically optimal, meaning as dimension grows they achieve approximation ratios arbitrarily close to the true value of K G [NR14].

The companion paper enlarges the space of previously known schemes via limiting Krivine schemes, obtained as limits of classical Krivine schemes of growing dimension. This enlarged search space is where both main results live.

Theorem 3.1 (Upper bound, abridged): There is an explicit limiting Krivine scheme, the cubic–quintic scheme, which shows K G pi over 2 (1+ sqrt 2) - 3.47 times 10-4. The scheme's partitions have cubic boundaries. "All previous constructions, including the two recent 10-5-scale improvements, were fixed low-dimensional schemes; this is the first improvement obtained by letting the dimension grow, and it answers affirmatively a question of Braverman et al. [BMMN11] on whether higher dimension helps."

Theorem 3.2 (Lower bound, abridged): The correlation function H(t) = b 1 t + b 3 t cubed + of every Krivine scheme satisfies the constraint b 3 2b 1 - 11 over 6. Combined with the optimality theorem of Naor and Regev, this implies K G 6 pi over 11 = 1.7135 The interesting feature is the reversal of strategy: Instead of constructing a hard instance, the proof establishes a ceiling on the performance of every scheme. This is the first lower bound on K G that does not proceed by constructing a gap instance.

Together, the two theorems give 6 pi over 11 K G pi over 2 (1+ sqrt 2) - 3.47 times 10-4, determining the tenths digit of K G to be 7.

The lower bound was obtained in collaboration with an AI research system. The cubic–quintic construction predates the current system and was found through conversation with GPT-5.5-Pro. The lower bound K G 6 pi/11 was discovered and first proved by the system; the authors have since verified the argument themselves.

The run used two frontier language models: a reasoning model (OpenAI GPT-5.5-Pro at maximal reasoning effort, replaced mid-run by GPT-5.6-Sol) and a coding agent (Anthropic Claude Code, running Claude Opus and later Claude Fable 5). Floating-point searches ran on a single four-GPU node, and every Arb-certified computation was redone in interval arithmetic on CPU.

The AI research system is a harness coupling two agents in distinct roles: (1) the reasoning agent serves as the brain that selects directions, develops arguments, specifies experiments, and audits the resulting claims, and (2) the coding agent serves as the executor that maintains the project repository, implements and runs experiments, retrieves literature, and drives the reasoning model through a scripted interface. The agents run in bounded sessions with no context surviving between sessions; continuity is carried by files, principally a problem statement, a single summary file serving as working memory, and append-only transcripts and experiment logs.

Work is organized into sessions of a few hours, with two to five running concurrently on distinct directions. Each session passes through fixed phases: orientation, selection of a focus, a research loop, and a closing audit producing a calibrated summary where every claim is tagged as proven, numerically supported, conjectural, or heuristic. The word theorem is reserved for statements the authors have additionally checked themselves.

Human operators steered the run asynchronously through text files, consisting of priorities, targets, audits of the run's own claims, and occasional mathematical pointers; about forty directives were issued over the run.

The run spanned June 16 to July 24, 2026, comprising roughly 240 research sessions. The reasoning model was called 2,091 times, consuming about 152 million tokens at an estimated 5,400 in API cost. The run's principal outcome is the lower bound K G 6 pi/11. Beyond it, the run produced system-tested upper bounds of 1.781801841033 and then 1.7813319810625639, improving on the cubic–quintic value, together with two stronger lower bounds (27π/49 ≈ 1.7311 and 51π/92 ≈ 1.7415). These are reported as machine-verified claims rather than theorems, as their certificates have not yet been human-verified.

The lower bound began with a plateauing search for a better upper bound. The system explored variants of limiting Krivine schemes but repeatedly encountered the same tradeoff: suppressing the unwanted nonlinear terms in the inverse majorant series also weakened the leading term. The run recorded this pattern but continued searching rather than treating repeated failures as evidence of a general obstruction.

The key human intervention was recognizing that repeated failures likely reflected a general analytic obstruction, and that proving such an obstruction would be mathematically valuable: by the optimality theorem of Naor and Regev, it would imply a lower bound on K G. The operators redirected the system away from searching for new schemes and asked it to synthesize accumulated failures, identify common structure, and attempt to prove a universal obstruction.

After further directives, the system found the central mathematical reframe and developed a complete proof. It expressed the obstruction as an affine inequality between the two leading coefficients of a scheme's correlation function. Because this inequality is preserved under averaging and limits, it extends to mixed and limiting schemes. The system then reduced required high-dimensional estimates to one-dimensional inequalities and produced the computer-assisted certificate, yielding K G 6 pi/11.

The paper notes: "The system was effective at technical execution... The human input was primarily of research judgement and mathematical taste: judging when a research direction has been somewhat exhausted, understanding that mathematical understanding and discoveries frequently come from synthesizing failures, and recognizing that a new lower-bound mechanism is much more interesting than a small numerical improvement to a known upper-bound method."

The paper presents a decomposition of long-horizon mathematical research into components: research state, research judgement, technical execution, and research-state representation. The system exhibited a consistent asymmetry: the system was strong at technical execution, but substantially less reliable at research judgement and at maintaining an accurate research state.

(1) Technical execution: strong. Once a sufficiently well-specified high-level action was fixed, the system was usually effective at thinking creatively and devising the mathematics and computations necessary to advancing the action. It drew upon vast mathematical knowledge and problem-solving skills to develop lemmas and proofs, and effectively ran and interpreted experiments.

(2) Research judgement: limited autonomy. The system did not reliably make these decisions at the program level. The initial upper-bound search is a clear example: several approaches failed for the same structural reason, yet the run opened another variation rather than asking whether the common obstruction was universal. "The relevant limitation was not an inability to perform the required reasoning. Once prompted to step back, synthesize, or reframe, the system often did so effectively. It was the failure to recognize, from the evolving state of the project, when such a change in reasoning mode was called for."

(3) Research-state representation: fragile. This functionality became more difficult as the run grew. The withdrawn upper bound in session 44 is a clear failure case: a fast numerical evaluator built in session 4 carried an explicit caveat that its score was safe only for exploration; the caveat did not survive later representations of the research state, and by session 44 the uncertified score had set the record. A feasibility criterion that would have invalidated the record was lost even earlier—proved in session 8, it disappeared in a later handoff and was eventually reproved from scratch by the audit that withdrew the record 25 days later. In both failures, the archive retained the original facts; it was the compressed state governing decisions that failed.

The paper hypothesizes an asymmetry in training data and feedback: there is a lot more experience with local, technical execution over global, long-horizon reasoning and planning. Mathematical papers, textbooks, and solved problems provide many examples of technical execution. AI models can be trained effectively on problems where final answers can be scored automatically, which roughly corresponds to technical execution skills.

Training data for research judgement is much rarer: "Finished mathematical papers rarely record the full process of discovery, including the abandoned approaches, the experiments performed, and decisions to pivot directions. Instead, they represent a polished final state, written for expositional clarity, rigor, and brevity. The weakness in research-state representation fits the same asymmetry: Curation is a global functionality: deciding what the program will later need to know is a prediction about its future. The active state was rewritten roughly two hundred times over the run, and each rewrite draws on a training genre, the finished mathematical paper, that states results and omits caveats, scope, and doubt. Therefore, iterated rewriting regresses toward that genre, and headline values survive retelling more reliably than their evidential status."

The human contribution entered in three areas: (1) supplying the initial research state, including the cubic–quintic framework and certification machinery; (2) supplying program-level research judgement through about forty directives, including the lower bound pivot; and (3) intervening in research-state representation, continuously changing the structure and guidelines for what information to store. The technical execution was left almost entirely to the system.

The paper notes recent AI successes in mathematics vary in method and human role: evaluator-guided search for record constructions, formal provers reaching medal-level performance on olympiad problems, and frontier reasoning models resolving open questions with varying human involvement. "To the best of our knowledge, this work is the first in-depth case study of a long-horizon human–AI collaboration on a mathematical research program: over several weeks, we accumulated intermediate results, explored and shelved various directions, and steered at the program level. The paper expects this collaborative mode, rather than full autonomy, to be the likeliest source of strongest results and thus the prevailing near-term form of AI-assisted mathematics."

The analysis suggests two complementary directions: "For AI research, improving research judgement and research-state representation may require training and evaluation on records of mathematics as a process, including failed approaches, strategic decisions, and evolving assessments of evidence. For mathematical practice, while these limitations persist, human expertise is likely to remain most valuable in these global functionalities: deciding when to persist or reframe a direction, and maintaining an accurate representation of accumulated progress."

Based on this paper, here are the specific improvements I can make to AI systems and the resulting capabilities:

• Improvement: Add a module that tracks repeated failures across multiple attempts and automatically detects when failures share a common structural cause (e.g., suppressing nonlinear terms also weakens leading term appearing across 10+ variants).

• Capability: The system will autonomously flag when a research direction has hit a fundamental obstruction and propose a pivot from search for better instance to prove universal limitation — without requiring human intervention.

• Improvement: Implement a structured memory system where every claim stored in the working summary retains its full provenance chain: original source, confidence level (proven/numerical/conjectural), validity conditions, and expiry/recheck triggers. Prevent loss of caveats during state compression by making them non-omittable metadata.

• Capability: The system will never again let an uncertified numerical score become a record or lose a feasibility criterion that invalidates results — eliminating the session-44 failure mode.

• Improvement: Add a heuristic that monitors for plateauing (e.g., no improvement over N consecutive sessions despite varied approaches) and automatically initiates a synthesis phase: clustering failures, extracting common constraints, and attempting to prove those constraints as universal theorems.

• Capability: The system will autonomously convert repeated empirical failures into formal lower-bound proofs, as happened with the K G 6 pi/11 result, without needing a human directive.

• Improvement: When rewriting the working memory summary (which happened 200 times), use a two-pass approach: first extract all claims with their confidence tags, then rewrite only the prose while forcing all caveats, scope limitations, and unverified statuses to be carried forward verbatim.

• Capability: The system will maintain accurate research state even after hundreds of iterations, preventing the regression toward polished paper genre that caused the loss of the feasibility criterion.

• Improvement: Train a separate research director module that operates at the program level (not session level), with access to cross-session statistics: failure rates by direction, resource allocation, and progress metrics. This module makes decisions about when to persist, pivot, or terminate research threads.

• Capability: The system will make strategic decisions like stop searching for upper bounds, pivot to proving lower bounds via obstruction autonomously, matching the human operator's key intervention.

• Improvement: Implement a mandatory post-mortem synthesis after every 5-10 failed attempts in the same direction, producing: (a) a list of common structural features across failures, (b) candidate universal constraints implied by those features, (c) a decision on whether to prove the constraint or continue searching.

• Capability: The system will systematically mine its own failures for general theorems, turning what would be dead ends into new mathematical results.

• Improvement: When compressing research state between sessions, use a lossy-but-safe encoding: all claims are stored with explicit confidence levels, and any claim whose confidence is below proven is automatically flagged for re-verification before being used in decisions.

• Capability: The system will never make program-level decisions based on unverified numerical results, preventing the uncertified score set the record failure.

• Improvement: Add a background process that continuously analyzes all session transcripts and experiment logs for recurring patterns (e.g., tradeoff between X and Y appears in 80% of failed attempts), and surfaces these patterns to the reasoning agent as potential universal obstructions.

• Capability: The system will proactively identify structural limitations across the entire research program, not just within individual sessions.

• Improvement: Train a module specifically on the 40 human directives from this run, learning the patterns of when humans intervene (e.g., after repeated failures in same direction, when numerical improvements are marginal, when a new proof mechanism is more valuable than incremental gains).

• Capability: The system will anticipate and preemptively make the judgments that humans had to provide, such as recognizing that a lower-bound proof is more valuable than a small upper-bound improvement.

• Improvement: Implement a system that automatically tracks which claims have human-verified certificates versus machine-verified only, and automatically escalates machine-verified claims to human verification when they become critical to the research program.

• Capability: The system will maintain clear separation between theorems and machine-verified claims, and will proactively push for human verification of claims that become load-bearing.

What the improved system can do: It can run a multi-week mathematical research program with minimal human oversight, autonomously detecting when a direction is exhausted, pivoting from search to proof-of-obstruction, maintaining accurate research state across hundreds of sessions, and producing verified theorems — while reserving human input for only the highest-level strategic decisions.

AI agents are increasingly used in mathematics research, but it is often unclear how to use them effectively. Towards this, we present an extensive case study of how AI was used to improve bounds on the Grothendieck constant K G, which captures the hardness between combinatorial problems and their continuous relaxations. Specifically, while the precise value of K G is not known, we recently tightened the best known bounds to [ 6 pi over 11 ;; K G ;; pi over 2 (1+ sqrt2) - 10-4.] Crucially, these improvements were achieved using an AI research system that could arrive at insights deemed novel by domain experts. We give a detailed discussion of our experience using AI for mathematics research, particularly touching upon its strengths and weaknesses, as well as our experience with creating ideal conditions for AI to arrive at breakthrough insights.