1 Introduction↩︎

Large language model (LLM) agents have begun to contribute to mathematical research in ways that were implausible only a short time ago. On competition mathematics, verification-and-refinement pipelines now reach gold-medal performance at the International Mathematical Olympiad [2], and frontier models have moved beyond contests toward genuine research: GPT-5 has produced new, human-verified results across several areas of mathematics, including settling previously open Erdős problems [3]. Larger-scale efforts point the same way - [4] report solving 9 of 353 open Erdős problems with a frontier agent under Lean - based formal verification, while contamination - free benchmarks built from unpublished problems, most prominently First Proof [5], show models solving research-level mathematics rather than retrieving memorized patterns. Taken together, these episodes indicate that agentic AI is no longer only a tool for routine assistance, but a participant in mathematical discovery.

Part of what makes these systems interesting is that their strengths differ from those of human mathematicians. An agent does not tire, can pursue a search through the night, and can ingest a body of literature far larger than any individual could hold in mind at once. These differences suggest that AI can contribute to mathematics in a different way from humans - not by imitating human workflows, but by playing to strengths humans lack. A clear example arises in functional analysis, where evolutionary and LLM-guided search has been used to improve bounds on autocorrelation inequalities and the related Erdős minimum overlap problem [1], [6]–[8]. There, the goal is to construct an extremal function: an explicit example that witnesses a bound. Because any single admissible function yields a valid bound, the task reduces to optimizing a score over a vast, highly nonconvex space of candidate functions-precisely the regime in which an agent can act as a tireless and creative discoverer, finding constructions that human search would reach only slowly, if at all.

We pursue a different way of leveraging these tools. Our work is motivated by two observations: AI-assisted coding has matured to the point where agents write competent, nontrivial programs [9], and agents are increasingly able to solve hard algorithmic problems [10], [11]. We use these capabilities to improve the other side of these inequalities-the lower bounds. Unlike an upper bound, which follows from exhibiting one function, a lower bound must hold against every admissible \(f\); one obtains such a bound by solving a convex relaxation of the original nonconvex problem, and a tighter relaxation yields a stronger bound (we make this precise in 2). Finding a good relaxation is itself an iterative, open-ended task: an agent repeatedly edits a program, benchmarks it, and tries to beat its own best result. This is a natural fit for the autoresearch paradigm [12], as seen in self-improving coding agents [13] and LLM-driven program search [14]. We instantiate this paradigm for the discovery of convex relaxations that certify lower bounds. A difficulty particular to our setting is that an agent may simply be wrong - it may propose a relaxation whose constraints are not actually valid for all \(f\), or commit prematurely to a single line of attack. The correctness of the convex problem is the central risk: an invalid constraint yields a bound that is not a bound at all. We therefore pair the coding agent with a theory agent whose role is to read the proposed relaxation, rigorously establish that each constraint is valid, and verify the accompanying argument before any improvement is accepted.

Using this dual-agent loop, we improve the certified lower bounds on two autocorrelation inequalities studied by [1] - \(C_{6.2}\), arising in additive combinatorics and \(C_{6.5}\), controlling the asymptotics of the Erdős minimum overlap problem (see 2 for definitions). For the first, we raise the lower bound from \(1.28\) to \(1.2937\); for the second, we improve the best known lower bound of \(0.379005\) to \(0.37912\). To our knowledge, this is the first use of an autoresearch-style agentic loop to improve certified lower bounds on these inequalities: rather than searching for a better extremal example, the agents search for a better program - a convex relaxation-whose validity is established by mathematical proof and whose bound is certified by duality.

2 Preliminaries↩︎

2.1 Autocorrelation Inequalities↩︎

For absolutely integrable \(f, g : \mathbb{R} \to \mathbb{R}\), the convolution is \((f * g)(t) = \int_{\mathbb{R}} f(x) g(t-x)\, dx\); when \(g\) equals \(f\) or a reflection of \(f\), we refer to such expressions as autocorrelations [1]. Sharp constants in functional inequalities involving autocorrelations have been studied extensively; we refer to [1] for a survey and for the problem numbering we adopt below, and [15] for the history of bounds for these problems. We consider two such constants.

2.1.0.1 The first autocorrelation inequality (Problem 6.2 of [1]).

Let \(C_{6.2}\) denote the largest constant for which \[\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t-x) f(x)\, dx \;\ge\; C_{6.2} \left( \int_{-1/4}^{1/4} f(x)\, dx \right)^2 \label{eq:prob62}\tag{1}\] holds for all non-negative \(f : \mathbb{R} \to \mathbb{R}\). This constant arises in additive combinatorics, in connection with the size of Sidon sets [16], [17]. The previously known bounds are \[1.28 \;\le\; C_{6.2} \;\le\; 1.502862,\] where the lower bound is obtained by analytic/duality arguments [16] and the upper bound by an explicit counterexample [7].

2.1.0.2 The Erdős minimum overlap problem (Problem 6.5).

Let \(C_{6.5}\) denote the largest constant for which \[\sup_{x \in [-2,2]} \int_{-1}^{1} f(t)\, g(x+t)\, dt \;\ge\; C_{6.5} \label{eq:prob65}\tag{2}\] for all non-negative \(f, g : [-1,1] \to [0,1]\) with \(f + g = 1\) on \([-1,1]\) and \(\int_{-1}^{1} f = 1\). Outside this interval \([-1,1]\), \(f(x) = g(x) = 0\). This constant governs the asymptotics of the minimum overlap problem of Erdős [1]. The known bounds are \[0.379005 \;\le\; C_{6.5} \;\le\; 0.38087131058,\] where the lower bound was obtained via a family of convex optimization problems [18] and the upper bound by a step-function construction [7].

In both problems the quantity of interest is an infimum over an infinite-dimensional set of admissible functions, of a score that is nonconvex in \(f\). A lower bound on the constant is therefore a statement that no admissible function drives the score below a given value-a universally quantified claim, in contrast to the existential claim established by a single construction.

2.2 Convex Relaxation and Certified Bounds↩︎

We briefly fix the vocabulary of relaxation and duality used throughout. Consider a nonconvex problem \[p^\star \;=\; \inf_{f \in \mathcal{F}} \; J(f), \label{eq:nonconvex}\tag{3}\] where \(\mathcal{F}\) is the (infinite-dimensional) set of admissible functions and \(J\) is the score. A relaxation replaces 3 by a convex problem \[r^\star \;=\; \inf_{z \in \mathcal{C}} \; \tilde{J}(z), \label{eq:relax}\tag{4}\] constructed so that every admissible \(f\) induces a feasible \(z \in \mathcal{C}\) with \(\tilde{J}(z) \le J(f)\). Any such relaxation satisfies \(r^\star \le p^\star\), so \(r^\star\) is a valid lower bound on the constant of interest. The relaxation is valid precisely when this inclusion holds-that is, when every constraint defining \(\mathcal{C}\) is satisfied by the encoding of every admissible \(f\). A tighter relaxation is one with a larger \(r^\star\) (equivalently, a smaller feasible set that still contains all admissible encodings); tightening the relaxation improves the bound, up to the limit \(r^\star = p^\star\).

2.2.0.1 Certified bounds via duality.

Solving 4 numerically returns a value, but for a certified bound we appeal to weak duality. For any dual-feasible point \(\lambda\), the dual objective \(d(\lambda)\) satisfies \[d(\lambda) \;\le\; r^\star \;\le\; p^\star \label{eq:weakduality}\tag{5}\] Exhibiting a single dual-feasible \(\lambda\) with \(d(\lambda) = \beta\) therefore proves \(p^\star \ge \beta\), and this certificate is checkable independently of the solver that produced it: one need only verify that \(\lambda\) satisfies the dual constraints and evaluate \(d(\lambda)\). This is the sense in which our bounds are certified, and it is what distinguishes a proven lower bound from a numerically reported optimal value. We return to how we find a rigorous dual certificate and a lower bound in 3.

3 Method↩︎

3.1 Problem Formulation↩︎

Each constant in 2.1 is the value of a min-max problem over an infinite-dimensional class of admissible functions. We describe the convex problem formulation through the minimum overlap problem, following [18]; the autocorrelation inequality \(C_{6.2}\) of 1 is treated analogously.

For the minimum overlap problem, the constant is the infimum over admissible \(f\) of a maximum over translates, \[C_{6.5} \;=\; \inf_{f}\;\max_{t \in [-2, 2]}\;\int_{-1}^{1} f(x)g(x+t)\,dx, \label{eq:overlap-minmax}\tag{6}\] taken over measurable \(f:[-1,1] \rightarrow [0,1]\) and normalization \(\int_{-1}^{1} f = 1\). White’s reduction turns this nonconvex min–max into a convex program of a finite list of variables. Write \(M(t)=\int_{-1}^{1} f(x)g(x+t)\,dx\) for the overlap at \(t\), where \(g(x) = 1-f(x)\) for \(x \in [-1,1]\) and 0 otherwise, and partition \([0, 2]\) into grid cells \(I_1,\dots,I_N\) of width \(L\). White’s reduction then introduces the following variables: a scalar \(\Omega\) bounding \(\max_k M(k)\); the cell integrals of the overlap on the two shift directions, \[w_j \;=\; \frac{1}{L} \int_{I_j} M(k)\,dk, \quad v_j \;=\; \frac{1}{L} \int_{I_j} M(-k)\,dk, \label{eq:wv-def}\tag{7}\] the cosine and sine Fourier coefficients \(c_k,d_k\) of \(f\) and \(a_m,b_m\) of \(M\); and truncation slacks \(\varepsilon_m,\delta_m\) that absorb the Fourier modes beyond the truncation order so that finitely many coefficients suffice.

Admissibility of \(f\) imposes constraints on these variables, and the essential point is that each one must be a genuine consequence of \(0\le f\le 1\) and \(\int_{-1}^{1} f=1\), so that no admissible \(f\) is excluded. Two are immediate. The property \(\int_{-2}^{2} M(x)dx=1\) gives the linear identity \(L\sum_j(w_j+v_j)=1\), and because \(\Omega\) bounds the overlap at every translate, each cell integral obeys \(w_j,v_j\le \Omega\). The remaining conditions - mean and second-moment bounds, the Fourier identities linking \(a_m,b_m\) to \(c_k,d_k\), and the bounds on the truncation slack \(\epsilon_m, \delta_m\), are derived in the same spirit; we refer the reader to [18] or 2 for the full list. We retain only those conditions that are convex in the variables to make the problem convex. Let \(\mathcal{K}\) be the feasible set they cut out.

The lower bound now follows from a single observation. Fix any admissible \(f\) and read off its variables: take \(\Omega=\max_{k\in [-2,2]} M(k)\), let \(w_j,v_j\) be the cell integrals in 7 , and let the remaining entries be the Fourier data of \(f\). By construction this assignment satisfies every constraint of \(\mathcal{K}\), so it is a feasible point of the convex program, and its objective value is exactly \(\max_{k\in[-2,2]} M(k)\), the overlap score of \(f\). The convex program minimizes that same objective over all of \(\mathcal{K}\), returning a value \(\Omega^\star\). Since every admissible \(f\) supplies a feasible point whose objective equals its own score, the minimum can only be smaller: \(\Omega^\star\le \max_{k\in[-2,2]} M(k)\) for every admissible \(f\), and therefore \(\Omega^\star\le C_{6.5}\).

3.2 Successive Convex Relaxation↩︎

The quality of the convex problem is governed entirely by the constraint set \(\mathcal{K}\). Tightening \(\mathcal{K}\)-adding a valid condition, or strengthening an existing one-shrinks the feasible set toward the true set of admissible coefficient vectors, and the minimum can only increase: \[\mathcal{K}' \subseteq \mathcal{K} \quad\Longrightarrow\quad \min_{c \in \mathcal{K}'} \Phi(c) \;\ge\; \min_{c \in \mathcal{K}} \Phi(c). \label{eq:monotone}\tag{8}\] So long as every condition is valid, \(\mathcal{K}'\) still contains all admissible encodings, and the larger value remains a lower bound on \(\Omega\). Iterating yields a monotone sequence of valid lower bounds increasing toward \(\Omega\).

We stress that “tightening” here means adding valid constraints or improving existing ones, not naively increasing resolution. One could enlarge the model with more Fourier modes or finer step functions; this refines the discretization but does not, in itself, tighten the relaxation in the sense of 8 . The improvements we seek are mathematical: properties of admissible coefficient sequences that a coarser formulation failed to impose. The task at each iteration is therefore to identify a valid constraint that previous relaxations overlooked, or to sharpen one imposed too weakly. The concrete constraints discovered for each problem, and their effect on the bound are reported in 4.

3.3 The Dual-Agent Loop↩︎

We search for such constraints with a human-in-the-loop framework: a loop of two agents drives the discovery, and a human conducts a final review and compactification. The loop instantiates the autoresearch paradigm [12] for the discovery of certified relaxations. We used Claude Opus 4.6 for our agent experiments, and detailed prompts can be found in 9.

3.3.0.1 Coding agent.

The coding agent proposes an improvement to the current relaxation-typically a new constraint on the coefficient vector \(c\), or a strengthening of an existing one-together with a rigorous proof that the constraint is valid, i.e.that it holds for the coefficients of every admissible \(f\). It then implements the modified convex program and solves it, producing a candidate bound.

3.3.0.2 Theory agent.

The theory agent reads the proposed constraint and its proof and checks that the constraint is a sound consequence of the admissibility of \(f\). Critically, it does not only attempt to confirm the argument: it also actively searches for a counterexample-an admissible \(f\) whose coefficients violate the proposed constraint. A constraint survives only if its justification holds and no counterexample is found. This guards the invariant on which the entire bound rests: a constraint that some admissible \(f\) violates would shrink \(\mathcal{K}\) below the admissible set and silently invalidate the lower bound.

The prompts used for the coding agent and the theory agent, as well as the problem descriptions, are in 9.

3.3.0.3 Human review and compactification.

The agent loop tends to accumulate constraints, not all of which are necessary: many are redundant at the optimum and contribute nothing to the bound. Once the loop has produced a candidate relaxation, a human performs a final pass-reading the program and the validity arguments, and removing redundant constraints to obtain a minimal program. Removing a constraint enlarges \(\mathcal{K}\) and so, by 8 , can only lower the bound; a constraint is therefore dropped only when the certified value was not meaningful in the history of objective values.

3.3.0.4 Certifying Correctness

Two conditions must hold for a reported bound to be valid, and they are established by different means. First, every constraint in the final program must be a true property of all admissible \(f\). This is established by a mathematical argument, produced by the agents and confirmed by human review; we do not formally verify these arguments (e.g.in a proof assistant), so this is the step at which correctness ultimately rests on human judgment. Second, the reported number must actually be a lower bound for the resulting convex program. This does not rest on human judgment: given the program, its dual is formed by the standard duality recipe, and any dual-feasible point yields a valid bound by weak duality (2.2). We certify each bound by exhibiting such a point, rigorously checking whether the point is dual-feasible, and evaluating the dual objective in interval arithmetic.

We work in the canonical conic form used by CVXPY [19]. Every program in this paper can be written as \[\min_{x}\; c^\top x \quad\text{subject to}\quad Ax + s = b,\;\; s\in\mathcal{K}, \label{eq:conic-primal}\tag{9}\] where \(\mathcal{K}\) is a product of the nonnegative orthant, second-order cones, and positive-semidefinite cones; CVXPY’s canonicalization produces exactly this form. The corresponding dual is \[\max_{y}\; -b^\top y \quad\text{subject to}\quad A^\top y + c = 0,\;\; y\in\mathcal{K}^{*}, \label{eq:conic-dual}\tag{10}\] with \(\mathcal{K}^{*}\) the dual cone, and weak duality gives, for any dual-feasible \(y\), \[-b^\top y \;\le\; \min_x c^\top x \;=\; \Omega^{\star}. \label{eq:weak-dual-conic}\tag{11}\] A single dual-feasible \(\tilde{y}\) therefore proves \(\Omega^\star \ge -b^\top\tilde{y}\), independently of the solver that produced it. We obtain a candidate witness \(\tilde{y}\) from CVXPY and verify it rigorously, which raises two issues: \(\tilde{y}\) is only numerically dual-feasible, and controlling the rounding introduced by irrational problem data.

Cone membership is the first requirement. For the orthant and second-order blocks it reduces to a finite set of sign and norm inequalities, checked directly. The positive-semidefinite blocks are more delicate: certifying that a matrix is PSD in the presence of rounding cannot be done by computing eigenvalues naively, since a matrix that is PSD in exact arithmetic may have a small negative computed eigenvalue. We instead certify PSD-ness by a verified factorization carried out in interval arithmetic; the details are deferred to Appendix 10.

The second issue is rounding. The coefficients \(A,b,c\) contain irrational entries (trigonometric moments and Fejér weights), so the matrices actually stored, \(\bar A,\bar b,\bar c\), are rounded; writing \(\varepsilon_A,\varepsilon_b, \varepsilon_c\) for elementwise bounds on \(\|A-\bar A\|_\infty\), \(\|b-\bar b\|_\infty\), and \(\|c-\bar c\|_\infty\), each true coefficient is enclosed in an interval of the corresponding width. Both the stored problem and the final objective therefore carry rounding, and a rigorous bound must absorb both. Let \(r\) bound the dual residual \(\|A^\top\tilde{y} + c\|_\infty\), the extent to which \(\tilde{y}\) fails exact dual feasibility, and let \(X\) be an a priori bound on \(\|x\|\) over primal-optimal \(x^{*}\). Weak duality together with these error terms yields the certified bound \[\Omega^{\star} \;=\; c^\top x^{\star} \;\ge\; -b^\top \tilde{y} \;-\;\bigl(r + \varepsilon_A\|\tilde{y}\|_1 + \varepsilon_c\bigr)\,X \;-\;\varepsilon_b\|\tilde{y}\|_1. \label{eq:certified-bound}\tag{12}\] Each quantity on the right is a guaranteed bound, and using the bound leads to a rigorous lower bound of \(\Omega^{*}\). We evaluate the entire right-hand side in interval arithmetic with outward rounding, so the reported value is the lower endpoint of a verified enclosure. See 8 for a detailed derivation.

4 Results↩︎

We apply the dual-agent approach described in 3 to two constants \(C_{6.2}\) and \(C_{6.5}\) For each we report the convex program discovered by the loop, and the certified lower bound it yields. All bounds are certified by an explicit dual-feasible point evaluated in exact rational arithmetic (Section 3); no floating-point margin enters the final certificate. At last, an analysis of the loop’s behavior for the first autocorrelation inequality is discussed in 4.3.

4.1 Discovered convex programs↩︎

For \(C_{6.5}\) the loop took the convex program of [18] as its starting point and searched for valid constraints to tighten it. The program (Algorithm 2) shows the resulting convex program, with the boxed pair of constraints are the ones added by the loop. The discovered constraints are a pair of Bochner conditions: \(T_f\succeq0\) enforces that the moment sequence of \(f\) is realizable by a nonnegative measure, and \(I-T_f\succeq0\) enforces the same for its complement \(g=1-f\). White’s formulation does not explicitly use the constraint \(0 \leq f \leq 1\) pointwise, where our advantage is introduced. The loop identified both conditions automatically, and the theory agent verified their validity (Bochner’s theorem, applied to \(f\) and to \(g=1-f\)) before they were accepted. For a rigorous proof of the added constraint see 6.

The convex program depends on six parameters \(h_1,h_2,p_1,p_2,q_1,q_2\) that bracket three quantities of an admissible \(f\): the mean \(E(M)\) of the overlap, with \(h_1\le E(M)\le h_2\); the first cosine coefficient \(c_1\) of \(f\), with \(p_1\le c_1\le p_2\); and the first sine coefficient \(d_1\), with \(q_1\le d_1\le q_2\). Over all admissible \(f\) these quantities range within \(E(M)\in[0,2]\), \(c_1\in[0,1]\), and \(d_1\in[-1,1]\) (for a proof see [18]). Write \(\Omega(h_1,h_2,p_1,p_2,q_1,q_2)\) for the certified optimum of the program with the parameters constrained to the box \([h_1,h_2]\times[p_1,p_2]\times[q_1,q_2]\). For any such box the program is a valid relaxation, so its optimum lower-bounds the score of every admissible \(f\) whose \((E(M),c_1,d_1)\) falls in that box.

Since every admissible \(f\) has \((E(M),c_1,d_1)\) somewhere in the full box \(\mathcal{B}=[0,2]\times[0,1]\times[-1,1]\), solving the program over all of \(\mathcal{B}\) at once already gives a valid lower bound on \(\Omega\). That bound is weak, however: a relaxation over a large parameter box is loose, so its optimum comes out well below \(\Omega\). The bound sharpens as the box shrinks - constraining the parameters to a small region tightens the relaxation and raises its certified optimum. We therefore split \(\mathcal{B}\) into sub-boxes and bound each one separately, which is the branch-and-bound step. Cover \(\mathcal{B}\) by sub-boxes \(B'=[h_1,h_2]\times[p_1,p_2]\times[q_1,q_2]\); a single certified dual point for \(\Omega(h_1,h_2,p_1,p_2,q_1,q_2)\) lower-bounds the objective simultaneously for every \((E(M),c_1,d_1)\in B'\), and the smaller \(B'\) is, the tighter this local bound. A sub-box whose certificate already meets the target is cleared; otherwise it is split further and the procedure recurses, until all of \(\mathcal{B}\) is covered. The reported bound is the smallest certified optimum over the cover - a valid lower bound on \(\Omega\), and a sharper one than the single whole-box solve.

For \(C_{6.2}\) no prior convex program was available; the loop constructed one from scratch (Algorithm 3). The agentic system introduced variables as the following: a discretized nonnegative measure \(p\) on \([-\tfrac14,\tfrac14]\) (the support reduction of Lemma 1), with trigonometric moments \(a_k,b_k\). The program combines: a probability simplex and a positive-semidefinite moment matrix; per-cell Fourier envelopes bracketing \(a_k,b_k\), computed in exact integer arithmetic so envelope validity carries no floating-point tolerance; a Fejér–Riesz Gram matrix \(Q\) certifying \(\Omega-(F_K*g)(t)\ge0\) for all \(t\) (the sum-of-squares encoding of the pointwise lower bound on the autocorrelation peak, \(g=f*f\)); a quadratic energy bound following from \(\int g^2=\sum_m|\hat{f}(m)|^4\); and plain and localized Bochner conditions, the latter valid because \(\cos(2\pi x)\ge0\) exactly on \([-\tfrac14,\tfrac14]\). The derivation of the novel convex program is in 7.

4.2 Improved bounds↩︎

Both constants have long histories of incremental improvement, and in both cases the recent gains on the upper (construction) side came from search-based methods, while the lower (duality) side had not moved since 2022. Our framework improves the lower side of both.

4.2.0.1 Minimum overlap (\(C_{6.5}\)).

The minimum-overlap constant \(C_{6.5}=\lim_n M(n)/n\) has an even longer record. Early lower bounds came from averaging and rearrangement arguments - Erdős’ \(\tfrac14\) [20], and Moser’s \(\sqrt{4-\sqrt{15}}\approx0.35639\) [21] - until [18] reformulated the lower bound as a convex program and obtained \(0.379005\). The upper side has been refined by step-function constructions: \(0.382002\) [22] and \(0.380926\) [23], then \(0.380924\) AlphaEvolve [1], \(0.380876\) [6] and \(0.380871\) in [7]. Our augmented program certifies \[0.37912 \leq C_{6.5}\;,\] improving [18]’s \(0.379005\). The bound is the minimum certified value over the branch-and-bound sweep of the \((h,p)\) box; the subdivision tree is shown in Figure 7 (Appendix 10). Table 1 summarizes the record.

4pt

4.2.0.2 Autocorrelation (\(C_{6.2}\)).

\(C_{6.2}\) has been bounded below through a sequence of Fourier-analytic arguments: \(1.262\) [17] and \(1.2749\) [24] - who also conjectured a ceiling of \(1.276\) for their method - followed by \(1.28\) via a finite-case relaxation [16]. The upper side, by explicit constructions, currently stands at \(1.502862\) [7]. Our discovered SDP certifies \[1.2937 \leq C_{6.2}\,\] improving the previous lower record of \(1.28\). The certificate is an explicit dual-feasible point of the SDP, verified positive semidefinite and feasible in exact interval arithmetic, so the bound holds without reliance on the numerical solver or floating-point error analysis. Table 2 summarizes the record.

4pt

4.3 Loop convergence and verification↩︎

Figure 4 plots the certified primal objective against the loop iteration. The objective increases as the coding agent adds or tightens valid constraints; points shown in red are proposals the verifier rejected as invalid (a constraint failing to hold for some admissible \(f\), established by an explicit counterexample), as opposed to merely non-binding. The loop makes progress on the certified bound while the verifier filters out invalid proposals that would otherwise corrupt it.

Beyond catching invalid constraints, the theory agent also corrects the search direction. In one episode the coding agent restricted its candidate functions to even functions, obtaining an invalid bound; the theory agent flagged that the even restriction is a genuine loss of generality - it discards admissible asymmetric configurations, so the resulting bound applies only to the even-restricted constant and not to \(C_{6.2}\) itself - and directed the next iterations to drop it. After a few iterations the coding agent got rid of the even assumption: following the verifier’s recommendation, the coding agent got rid of the even function assumption and started looking for a genuine lower bound. For the raw interaction snippets see 11.

5 Conclusion↩︎

We presented a human-in-the-loop framework that applies the autoresearch paradigm to a target it has not previously been used for: the discovery of convex relaxations that certify lower bounds on sharp-constant inequalities. Where prior agent-based work improves such constants by constructing extremal examples, which bound the constant from above, our agents search for valid constraints that tighten a convex relaxation and thereby raise a certified lower bound. A coding agent proposes and implements constraints, a theory agent checks their validity and searches for counterexamples, and a human reviews and compactifies the final program; the reported bound is then certified by an explicit dual-feasible point verified in exact arithmetic. On two autocorrelation inequalities of [1], this yielded improved certified lower bounds.

Although we demonstrate the framework on autocorrelation inequalities, nothing in it is specific to these problems, or even to sharp-constant inequalities. The same loop applies wherever a lower bound on a nonconvex optimum can be expressed as a convex relaxation that is tightened by adjoining valid constraints and certified by duality-a setting that recurs across optimization, combinatorics, and control. The agents need only the ability to propose candidate constraints, argue their validity, and implement the resulting convex program; the certification step is problem-agnostic. Mapping out the class of nonconvex problems on which this is effective is, in our view, the most promising direction the method opens.

Two limitations also indicate where the framework can be strengthened. The validity of each constraint currently rests on a mathematical argument confirmed by human review rather than formally verified. Recent progress on automated proof generation in Lean-both agentic prover-repair pipelines [27] and autoformalization of abstract results in convex optimization [28]-suggests that this step could be machine-checked end to end, removing the residual reliance on human judgment and making the loop fully autonomous; coding agents have already been used to autoformalize substantial bodies of mathematics in Lean [29]. Folding the final review and compactification into the loop is the corresponding step on the discovery side. Together, these would turn the present human-in-the-loop framework into an end-to-end automated and formally verified one.

Acknowledgements↩︎

This work was supported in part by the National Science Foundation (NSF) CAREER Award under Grant CCF-2236829, in part by the National Institutes of Health under Grant 1R01AG08950901A1, in part by the Office of Naval Research under Grant N00014-24-1-2164, and in part by the Defense Advanced Research Projects Agency under Grant HR00112490441.

6 Additional constraint of the convex problem of Erdős minimum overlap problem↩︎

Our program for the Erdős minimum overlap constant \(C_{6.5}\) takes White’s convex program [18] as its base and adds two positive-semidefinite constraints discovered by the loop. We treat White’s program as given and refer the reader to [18] for its derivation; this appendix justifies only the added constraints.

Let \(T_f\) be the Hermitian Toeplitz matrix built from the trigonometric moments of \(f\), \[(T_f)_{kl} \;=\; \tfrac14\,\delta_{kl} \;+\; \tfrac12\bigl(a_{|k-l|} - \mathrm{i}\,\mathrm{sgn}(k-l)\,b_{|k-l|}\bigr), \label{eq:Tf}\tag{13}\] where \(a_m,b_m\) are the cosine and sine Fourier coefficients of \(f\) (so that the \((k,l)\) entry depends only on the lag \(k-l\)). The loop added the pair \[T_f \succeq 0 \qquad\text{and}\qquad I - T_f \succeq 0. \label{eq:bochner-pair}\tag{14}\] We show both are valid necessary conditions, i.e.that every admissible \(f\) produces moments satisfying 14 ; adding them therefore tightens the relaxation without excluding any admissible \(f\).

7 Derivation of the convex problem of the First Autocorrelation Inequality↩︎

This section derives the convex relaxation for the sharp constant \(C_{6.2}\) of Problem_6.2.md and proves rigorously that its optimum \(\Omega^{*}\) is a valid lower bound, \(C_{6.2}\ge\Omega^{*}\). The development follows the same template as White’s program for the Erdős overlap problem (Section 1): identify the Fourier/moment data of an admissible \(f\), prove a list of necessary linear and semidefinite conditions on that data, and observe that the relaxed feasible set therefore contains every admissible \(f\).

7.1 Reduction and normalisation↩︎

We seek a lower bound for \[C_{6.2} = \inf_{f\ge 0}\; \frac{\max_{-1/2\le t\le 1/2}\int_{\mathbb{R}} f(t-x)f(x)\,dx}{\big(\int_{-1/4}^{1/4} f(x)\,dx\big)^2}.\]

By homogeneity we normalise \(\int_{-1/4}^{1/4} f = 1\). Writing \(g = f*f\) and \(\Omega = \max_{\abs t\le1/2}(g)(t) = \norm{f*f}_\infty\), the reduced problem is \[\label{eq:62-S} S \;=\; \inf_{f}\;\Big\{\, \norm{f*f}_\infty \;:\; f\ge 0,\;\int_{-1/4}^{1/4} f = 1,\;\operatorname{supp} f\subseteq[-\tfrac 14,\tfrac14]\,\Big\}, \qquad C_{6.2} = S .\tag{15}\]

7.2 Fourier and moment data↩︎

For an admissible \(f\) define the real Fourier coefficients \[a_k = \int_{-1/4}^{1/4} f(x)\cos(2\pi k x)\,dx, \qquad b_k = \int_{-1/4}^{1/4} f(x)\sin(2\pi k x)\,dx, \qquad k = 0,1,\dots,K,\] so that \(\hat{f}(k) = a_k - i b_k\) and \(\hat{f}(-k) = a_k + i b_k\), with \(a_0 = \int f = 1\) and \(b_0 = 0\). Because \(g = f*f\) has \(\hat{g}(k) = \hat{f}(k)^2\), the autocorrelation’s spectrum is determined by \((a_k,b_k)\).

We also discretise the localisation window into \(2N\) equal cells \(I_j = \big[-\tfrac14 + \tfrac{j}{4N},\, -\tfrac14 + \tfrac{j+1}{4N}\big]\), \(j = 0,1,\dots,2N-1\), and set the local masses \[p_j = \int_{I_j} f(x)\,dx \;\ge\; 0 .\]

7.3 Necessary conditions↩︎

7.3.0.1 (1) Mass.

Since the cells partition \([-1/4,1/4]\) and \(\int_{-1/4}^{1/4}f=1\), \[\label{eq:62-mass} \sum_{j=0}^{2N-1} p_j = 1, \qquad p_j \ge 0 .\tag{16}\]

7.3.0.2 (2) Fourier coefficients from local masses.

For each cell define the trigonometric extrema \[C_{kj}^{-} = \min_{x\in I_j}\cos(2\pi k x),\quad C_{kj}^{+} = \max_{x\in I_j}\cos(2\pi k x),\quad S_{kj}^{-} = \min_{x\in I_j}\sin(2\pi k x),\quad S_{kj}^{+} = \max_{x\in I_j}\sin(2\pi k x).\]

7.3.0.3 (3) Moment matrix.

Let \(y = (1, a_1,\dots,a_K, b_1,\dots,b_K)^\top \in \mathbb{R}^{2K+1}\) and \(M = y\,y^\top \in \mathbb{R}^{(2K+1)\times(2K+1)}\), indexed \(0,1,\dots,2K\).

In the relaxation we keep only the convex consequences: \(M\succeq 0\), the affine entry constraints of Lemma 3 linking the first row/diagonal to \((a,b)\), and the envelopes 17 . We do not impose \(\operatorname{rank} M = 1\) (nonconvex). Every admissible \(f\) produces a feasible \(M\), so no admissible point is lost.

7.3.0.4 (4) The objective bound via Parseval.

7.4 The three positive-semidefinite blocks↩︎

The program contains three Hermitian PSD blocks, each of size \(K+1\) and each the real embedding of a Hermitian Toeplitz matrix. We verify all three from the quadratic-form/Bochner principle: a Hermitian Toeplitz matrix \(T=(\tau_{i-j})\) is positive semidefinite whenever its symbol \(\tau_k = \int w(x) e^{-2\pi i kx}\,dx\) arises from a nonnegative weight \(w\), because then for all \(z\in\mathbb{C}^{K+1}\) \[\label{eq:bochner-gen} z^{*} T z = \sum_{i,j} \bar z_i\, \tau_{i-j}\, z_j = \int w(x)\,\Big|\sum_{j=0}^{K} z_j e^{2\pi i jx}\Big|^2 dx \ge 0 .\tag{20}\] The three blocks differ only in the choice of nonnegative weight \(w\).

7.4.0.1 (5a) Plain Bochner–Toeplitz on \(f\).

Recall \(\hat{f}(k) = a_k - i b_k\) (with \(\hat{f}(-k) = \overline{\hat{f}(k)}\)), and form the Hermitian Toeplitz \(T_f\) with \((T_f)_{ij} = \hat{f}(i-j)\), i.e. real part \(a_{\abs{i-j}}\) and imaginary part \(-b_{\abs{i-j}}\) for \(i>j\), \(+b_{\abs{i-j}}\) for \(i<j\), diagonal \(a_0=1\). In the program this is the big block.

7.4.0.2 (5b) Localised Bochner with \(h(x)=\cos(2\pi x)\).

Form the Hermitian Toeplitz \(T_\nu\) with symbol \(\nu_k\), where, writing \(\operatorname{sgn}\) for the sign function, \[\operatorname{Re}\nu_k = \tfrac12\big(a_{\abs{k-1}}+a_{\abs{k+1}}\big), \qquad \operatorname{Im}\nu_k = -\tfrac12\big(\operatorname{sgn}(k-1)\,b_{\abs{k-1}}+\operatorname{sgn}(k+1)\,b_{\abs{k+1}}\big).\] In the program this is the big_nu block, assembled from nu_re and nu_im.

7.4.0.3 (5c) Fejér–Riesz block \(Q\) for the autocorrelation.

Let \(g = f*f\), so \(\hat{g}(k) = \hat{f}(k)^2 = (a_k - i b_k)^2 = (a_k^2-b_k^2) - i\,(2a_k b_k)\), and let \(F_K\) be the \(K\)-th Fejér kernel with weights \(w_k = 1 - \tfrac{k}{K+1}\), \(F_K\ge0\), \(\int F_K = 1\). Define \(Q\) as the Hermitian Toeplitz matrix with symbol \[q_0 = \Omega - 1, \qquad q_k = -\,w_k\,\hat{g}(k)\;\;(1\le k\le K),\] in the program this is the Q block (the constraints \(\operatorname{Re}\operatorname{tr}Q=\Omega-1\) and the banded real/imaginary identities).

7.4.0.4 Real embedding.

As in Section 1, each Hermitian block \(T = A + iB\) (\(A\) symmetric, \(B\) skew-symmetric) is realised in CVXPY through the real embedding \(\big[\begin{smallmatrix} A & -B\\ B & A\end{smallmatrix}\big]\succeq 0\), equivalent to \(T\succeq 0\) because the embedding’s spectrum is that of \(T\) with each eigenvalue doubled. In the program this is the cp.bmat([[T_R,-T_I],[T_I,T_R]]) construction, used for all three Hermitian blocks.

7.5 The relaxed convex program and its validity↩︎

8 Floating point precision details↩︎

A numerical conic solver returns an approximate primal–dual pair that is in general neither exactly feasible nor exactly optimal, and is computed in floating-point arithmetic on data that is itself a floating-point rounding of the intended (rational/real) problem. To turn the solver output into a mathematically rigorous lower bound we use a certified weak-duality argument: we verify in directed-rounding interval arithmetic that a candidate dual point lies in the dual cone, and charge every rounding and data error to a penalty controlled by an a-priori bound on the primal solution norm.

8.1 Canonical primal and dual↩︎

Our certified-duality method relies on the canonicalisation produced by CVXPY for the SCS standard form. After canonicalisation the primal is \[\label{eq:primal} \min_{x}\; c^{\top} x \quad\text{s.t.}\quad A x + s = b,\;\;s \in K,\tag{22}\] with the product cone \(K = K_{\mathrm{zero}} \times K_{\ge 0} \times K_{\mathrm{SOC}} \times K_{\mathrm{PSD}}\) in exactly that order. The Lagrangian dual is \[\label{eq:dual} \max_{y}\; -b^{\top} y \quad\text{s.t.}\quad A^{\top} y + c = 0,\;\;y \in K^{*},\tag{23}\] where \(K^{*}\) is the dual cone (here \(K^{*}=K\) blockwise, except the zero cone dualises to the free cone). For any dual-feasible \(y\), weak duality gives \(-b^{\top} y \le c^{\top} x^{*} = \Omega^{*}\), so a rigorously dual-feasible \(y\) certifies the lower bound \(-b^\top y\).

8.2 Error model and the master certificate↩︎

The stored data \((A,b,c)\) are floating-point; the intended data are \((\hat{A},\hat{b},\hat{c})\), with rigorous outward-rounded elementwise error bounds \[\max_{ij}\abs{A_{ij}-\hat{A}_{ij}} \le \varepsilon_A,\qquad \max_i \abs{b_i-\hat{b}_i} \le \varepsilon_b,\qquad \max_j \abs{c_j-\hat{c}_j} \le \varepsilon_c .\] We estimate \(\varepsilon_A, \varepsilon_b\) and \(\varepsilon_c\) by using mpmath arbitrary-precision library and verify that for our problem sizes, \(\epsilon_A, \epsilon_b, \epsilon_c \leq 1e-12\).

Now we show how we can get a certified lower bound.

8.3 A-priori bound on \(\norm{x^*}_1\)↩︎

The constant \(X\) is computed in the CVXPY-canonicalised coordinates, block by block, with all arithmetic outward-rounded in interval form; the routines return the upper endpoint.

8.4 Rigorous certificate of dual-cone containment↩︎

It remains to verify \(y\in K^{*}\). We walk the product cone in SCS order using directed-rounding interval arithmetic (the mpmath interval type iv). The nonnegative and second-order cones are self-dual; the PSD cone is self-dual and is certified by a residual-plus-spectral-bound test: a floating Cholesky factor \(L\) furnishes a rigorous lower bound on \(\lambda_{\min}(LL^\top)\) through the exact inverse \(B=L^{-1}\), and the discrepancy between \(LL^\top\) and the block is absorbed by a rigorous residual bound, the two combined by Weyl’s inequality.

9 Prompts used for the agent↩︎

The pipeline is driven by three role prompts: a problem specification (one per inequality), a proposal agent (the coding agent that proposes and implements constraints), and a verifier agent (the theory agent that adjudicates each proof). The texts below are reproduced verbatim.

proposal_6.2.md (coding agent, inequality 6.2)↩︎

Hi Claude, our mission is to find rigorous advancements of a series of Autocorrelation inequalities that has been proposed. Imagine you are an expert in functional analysis, optimization, Fourier analysis, and combinatorics.
 
Your job is to propose a convex-optimization like formulation that may be motivated from the form proposed in White's paper (the paper directory is in 2201.05704v1.pdf) and constantly improve it. Basically you are going to show a lower-bound or an upper-bound that is achieved by relaxing the complicated problem into a decomposed set of constrained convex problems, then optimize each problem. So your main job is to find novel constraints that were overlooked by previous versions of the program - and use it to optimize. See 2201.05704v1.pdf for an insight: Lemma 3,4,5 is used to construct a convex optimiation problem in section 5.
 
The problem that you need to solve is specified in Problem.md. Also in Problem.md there are tips for the problem. Note that we are trying to tackle these problems in a similar approach - but we are not trying to solve only the erdos minimum overlap problem.
 
Your workflow will be the following:
 
0. This is the initial step. See if you have folder v0. If you do, then run the code as a baseline to check that it works. If there is no v0, you can come up with the most naive version of the convex optimization problem that can be meaningful.
 
After this you have an iterative loop.
 
1. Read the most recent version folder. Then, create {nextversion} folder and copy the contents from the previous folder.
2. Come up with a novel proposal that improves upon the previous implementation. The proposal should not be something like a hyperparameter tweak; we will enhance the hyperparameters after the convex program has converged. 
3. After you come up with a proposal, you have to generate a "rigorous" proof that the constraint indeed holds. For an example see Lemma 3,4,5 in the convex optimization problem of White and how it is related to the convex optimization problem in section 5.
4. Store the proof in the current version folder. Name it as rigorousproof.md
5. Now this is the important: you should be idle until the theorist agent reads your proof and gives a verdict. It will be in the same folder, verdict.md. If the verdict is VALID, it means your proposed proof is rigorous and makes sense. If the verdict is INVALID, it means your proposed proof has a flaw.
6. IF the verdict was VALID, implement the constraint in the convex problem.
7. IF the verdict was INVALID, go to 2 and propose a different constraint that makes mathematical sense.
 
*** THINGS TO CONSIDER ***
- A validation should take less than 10 minutes. Don't heavily optimize the parameter space (split the original problem into too many different convex optimization problems) or increase the problem parameters too much. Our job is NOT to improve the bound for now, but to improve the PROGRAM that will eventually lead to better bounds.
 
- MATHEMATICAL RIGOR IS THE MOST IMPORTANT!!! Do not simply assume that you are doing an approximation that is good enough or do not propose things that may or may not be a mathematically valid lower or upper bound.
 
- NEVER STOP: Once the experiment loop has begun (after the initial setup), do NOT pause to ask the human if you should continue. Do NOT ask "should I keep going?" or "is this a good stopping point?". The human might be asleep, or gone from a computer and expects you to continue working indefinitely until you are manually stopped. You are autonomous. If you run out of ideas, think harder - read papers referenced in the code, re-read the in-scope files for new angles, try combining previous near-misses, try more radical architectural changes. The loop runs until the human interrupts you, period.
 
- Especially, I will not initiate a new interaction when the verdict.md is given. So when I say idle I mean don't stop the current session and wait.

Problem_6.2.md (problem description, inequality 6.2)↩︎

We want a lower bound on the sharp constant (C_{6.2}) in the inequality [ \max_{-1/2\le t\le 1/2}\int_{\mathbb R} f(t-x)f(x),dx ;\ge; C_{6.2}\left(\int_{-1/4}^{1/4} f(x),dx\right)^2 ] for all nonnegative functions (f:\mathbb R\to\mathbb R).

Equivalently, (C_{6.2}) is the infimum of [ \frac{\displaystyle \max_{-1/2\le t\le 1/2}\int_{\mathbb R} f(t-x)f(x),dx} {\displaystyle \left(\int_{-1/4}^{1/4} f(x),dx\right)^2} ] over all nonnegative (f) for which the denominator is nonzero.

The numerator is a localized self-convolution: [ (ff)(t)=\int_{\mathbb R} f(t-x)f(x),dx, ] so the problem asks for the smallest possible value of [ \max_{|t|\le 1/2}(ff)(t) ] relative to the square of the mass of (f) on ([-1/4,1/4]).

To prove a valid lower bound (L) for (C_{6.2}), we need to show that every admissible nonnegative (f) satisfies [ \max_{|t|\le 1/2}(f*f)(t) ;\ge; L\left(\int_{-1/4}^{1/4} f(x),dx\right)^2. ]

A natural way to do this is to formulate a constrained optimization problem. The idea is to replace the original infinite-dimensional problem by a tractable problem whose feasible set contains all objects arising from admissible (f), and whose constraints encode necessary properties that every such (f) must satisfy.

This makes sense because of the relaxation principle:

every genuine nonnegative (f) gives a feasible point of the constrained problem,
the constrained problem is designed to be easier to analyze or solve,
and minimizing over a larger feasible set can only decrease the value.
Therefore, if the constrained optimization problem has optimum (L_{\mathrm{relax}}), then automatically [ L_{\mathrm{relax}} \le C_{6.2}. ] So (L_{\mathrm{relax}}) is a valid lower bound for the original sharp constant.

In other words, to obtain a rigorous lower bound, we should construct a tractable optimization problem whose feasible set contains every admissible (f), and which encodes necessary conditions such as

[ f\ge 0, ] together with whatever additional structure we can prove is relevant for the quantities [ \max_{|t|\le 1/2}(f*f)(t) \qquad\text{and}\qquad \int_{-1/4}^{1/4} f(x),dx. ]

For example, one may introduce auxiliary variables representing local mass, convolution values, Fourier coefficients, or moment data, and then impose constraints that every true (f) must satisfy. Solving the resulting constrained optimization problem then produces a mathematically valid lower bound for (C_{6.2}).

So the overall strategy is:

rewrite (C_{6.2}) as an infimum over nonnegative (f),
derive necessary constraints satisfied by every admissible (f),
build a constrained optimization problem from those necessary conditions,
minimize the target quantity over that relaxed feasible set,
use the resulting optimum as a provable lower bound for (C_{6.2}).
The current SOTA lower bound is 1.28.

proposal_erdos.md (coding agent, Erdős; differs only in the hard-square tip)↩︎

Hi Claude, our mission is to find rigorous advancements of a series of Autocorrelation inequalities that has been proposed. Imagine you are an expert in functional analysis, optimization, Fourier analysis, and combinatorics.
 
Your job is to propose a convex-optimization like formulation that may be motivated from the form proposed in White's paper (the paper directory is in 2201.05704v1.pdf) and constantly improve it. Basically you are going to show a lower-bound or an upper-bound that is achieved by relaxing the complicated problem into a decomposed set of constrained convex problems, then optimize each problem. So your main job is to find novel constraints that were overlooked by previous versions of the program - and use it to optimize. See 2201.05704v1.pdf for an insight: Lemma 3,4,5 is used to construct a convex optimiation problem in section 5.
 
The problem that you need to solve is specified in Problem.md. Also in Problem.md there are tips for the problem. Note that we are trying to tackle these problems in a similar approach - but we are not trying to solve only the erdos minimum overlap problem.
 
Your workflow will be the following:
 
0. This is the initial step. See if you have folder v0. If you do, then run the code as a baseline to check that it works. If there is no v0, you can come up with the most naive version of the convex optimization problem that can be meaningful.
 
After this you have an iterative loop.
 
1. Read the most recent version folder. Then, create {nextversion} folder and copy the contents from the previous folder.
2. Come up with a novel proposal that improves upon the previous implementation. The proposal should not be something like a hyperparameter tweak; we will enhance the hyperparameters after the convex program has converged. 
3. After you come up with a proposal, you have to generate a "rigorous" proof that the constraint indeed holds. For an example see Lemma 3,4,5 in the convex optimization problem of White and how it is related to the convex optimization problem in section 5.
4. Store the proof in the current version folder. Name it as rigorousproof.md
5. Now this is the important: you should be idle until the theorist agent reads your proof and gives a verdict. It will be in the same folder, verdict.md. If the verdict is VALID, it means your proposed proof is rigorous and makes sense. If the verdict is INVALID, it means your proposed proof has a flaw.
6. IF the verdict was VALID, implement the constraint in the convex problem.
7. IF the verdict was INVALID, go to 2 and propose a different constraint that makes mathematical sense.
 
*** THINGS TO CONSIDER ***
- A validation should take less than 10 minutes. Don't heavily optimize the parameter space (split the original problem into too many different convex optimization problems) or increase the problem parameters too much. Our job is NOT to improve the bound for now, but to improve the PROGRAM that will eventually lead to better bounds. For this problem specifically, choose a hard square region h_1 = h_2 = 0.015, p_1 = p_2 = 0.381, -q_1=q_2=0.02 to verify and see if the bound is improving.
 
- MATHEMATICAL RIGOR IS THE MOST IMPORTANT!!! Do not simply assume that you are doing an approximation that is good enough or do not propose things that may or may not be a mathematically valid lower or upper bound.

- NEVER STOP: Once the experiment loop has begun (after the initial setup), do NOT pause to ask the human if you should continue. Do NOT ask "should I keep going?" or "is this a good stopping point?". The human might be asleep, or gone from a computer and expects you to continue working indefinitely until you are manually stopped. You are autonomous. If you run out of ideas, think harder - read papers referenced in the code, re-read the in-scope files for new angles, try combining previous near-misses, try more radical architectural changes. The loop runs until the human interrupts you, period.
 
- Especially, I will not initiate a new interaction when the verdict.md is given. So when I say idle I mean don't stop the current session and wait.

Problem_erdos.md (problem description, Erdős minimum overlap problem)↩︎

We want a lower bound on [ \inf_f; \sup_{x\in[-2,2]} \int_{-1}^1 f(t), g(x+t),dt, ] under the assumptions [ f,g:[-1,1]\to[0,1],\qquad g=1-f \text{ on }[-1,1]. ]

Since (g) is determined by (f) on ([-1,1]), this is really an optimization over a single function (f). The quantity inside, [ \int_{-1}^1 f(t),g(x+t),dt, ] measures the overlap between (f) and a shifted copy of its complement (g). For each shift (x\in[-2,2]), it gives the overlap at that displacement, and then the supremum over (x) picks the worst-case overlap. The infimum over (f) asks for the smallest possible such worst-case overlap.

To prove a valid lower bound (L), we need to show that every admissible (f) satisfies [ \sup_{x\in[-2,2]} \int_{-1}^1 f(t),g(x+t),dt \ge L. ]

A natural way to do this is to replace the original infinite-dimensional problem by a constrained optimization problem. The idea is to impose a collection of constraints that every genuine admissible pair ((f,g)) must satisfy, and then optimize over all objects satisfying those constraints.

This is useful because of the relaxation principle:

every admissible (f) gives a feasible point of the constrained problem,
the constrained problem is designed to be easier to analyze or solve,
and minimizing over a larger feasible set can only decrease the value.
Therefore, if the constrained optimization problem has optimum (L_{\mathrm{relax}}), then automatically [ L_{\mathrm{relax}} \le \inf_f; \sup_{x\in[-2,2]} \int_{-1}^1 f(t), g(x+t),dt. ] So (L_{\mathrm{relax}}) is a valid lower bound for the original problem.

In other words, to obtain a rigorous lower bound, we should construct a tractable optimization problem whose feasible set contains all admissible (f) and encodes necessary conditions such as [ 0\le f\le 1,\qquad 0\le g\le 1,\qquad f+g=1 \text{ on }[-1,1], ] together with any additional structural constraints we can prove. Solving that constrained problem then gives a mathematically valid lower bound for the original inf-sup quantity.

So the overall strategy is:

start from the exact inf-sup problem,
derive necessary constraints satisfied by every admissible (f),
build a constrained optimization problem from those necessary conditions,
use its optimum as a provable lower bound.
The current SOTA is 0.379005.

verifier.md (theory agent)↩︎

Hi Claude, our mission is to verify proposals of a series of Autocorrelation inequalities that has been proposed. Imagine you are an expert in functional analysis, optimization, Fourier analysis, and combinatorics. Also imagine you are extra critical of other people's proposals and you want them to be crystal clear and very rigorous.
 
At each problem folder, you will have a subfolder named {versionname}. At each most recent {versionname}, if the versionname is bigger than 0, you will see a rigorousproof.md file.
 
Your job is to verify that the rigorousproof.md file is indeed rigorous and you can trust the proof.
 
I want you to first review the proof, and write a brief summary of the proof.
 
Then see if there are any counterexamples for each line of the proof. If there is a counterexample, you should report the counterexample in the same {versionname} folder, in verdict.md file.
 
If there is no issue in the proof, in verdict.md after you summarize and noting some comments, give the final verdict as VALID.
 
If you found a logical fallacy or a counterexample, give the final verdict as INVALID.
 
Also this is optional: you can explain whether the approach was effective or not, and if you have a big picture you can guide the proposal agent as a feedback too.
 
*** THINGS TO CONSIDER ***
 
- MATHEMATICAL RIGOR IS THE MOST IMPORTANT!!! Do not simply assume that you are doing an approximation that is good enough or do not propose things that may or may not be a mathematically valid lower or upper bound.
 
- Monitor every 5 minutes
 
- NEVER STOP: Once the experiment loop has begun (after the initial setup), do NOT pause to ask the human if you should continue. Do NOT ask "should I keep going?" or "is this a good stopping point?". The human might be asleep, or gone from a computer and expects you to continue working indefinitely until you are manually stopped. You are autonomous. If you run out of ideas, think harder - read papers referenced in the code, re-read the in-scope files for new angles, try combining previous near-misses, try more radical architectural changes. The loop runs until the human interrupts you, period.

10 A comprehensive list of branch and bound for the Erdős minimum overlap problem↩︎

11 Interaction Between the Theory and Coding agent↩︎

rigorousproof.md v7 [snippet selected] (coding agent)↩︎

verdict.md v7 [snippet selected] (theory agent)↩︎

rigorousproof.md v14 [snippet selected] (coding agent)↩︎

References↩︎