Summary (Overview)

• LongTails is a novel framework for automated research in mathematical optimization that uses Lean 4 formal verification to discover and prove oracle-complexity bounds.
• The framework separates a Setup (problem class, assumptions, available information, success criterion) from a Complexity (sufficient oracle-call budget), enabling agents to search for better algorithms and proofs while the Setup remains fixed.
• Using this framework, the authors have obtained more than 100 new theoretical results across diverse optimization areas including generalized smoothness, heavy-tailed noise, finite-sum optimization, composite optimization, higher-order methods, and zeroth-order optimization.
• Key technical achievements include improved complexity bounds for generalized smooth convex optimization, first convergence guarantees for coordinate Adam under heavy-tailed noise with optimal accuracy exponent, and accelerated guarantees for BFGS on linear-predictor objectives.
• To the best of the authors' knowledge, LongTails is the first framework to scale automated research in optimization across such a broad range of problems with formally verified theoretical guarantees.

Introduction and Theoretical Foundation

The paper addresses the growing intersection of agentic AI systems with mathematical research. While systems like OpenAI's have demonstrated success in proving mathematical theorems, the authors identify a gap in mathematical optimization: the need to not only design new algorithms but also prove their theoretical convergence rates are sound and superior to existing methods.

The fundamental structure of optimization problems motivates the framework design:

"Given a setup, we not only want to design a new method but, more importantly, prove that its theoretical convergence rate is sound and ideally better than those of previous methods."

The theoretical foundation rests on the classical problem of convex optimization with L-smooth functions:

$$\min_{x \in \mathbb{R}^d} f(x)$$

where $f$ is differentiable and convex with Lipschitz-continuous gradient: $\|\nabla f(x) - \nabla f(y)\| \leq L\|x - y\|$ for all $x, y \in \mathbb{R}^d$.

The accelerated gradient method achieves the accuracy criterion within:

$$N = \left\lceil \sqrt{\frac{2LR^2}{\varepsilon}} \right\rceil \tag{1}$$

gradient queries, where $R \geq \|x_0 - x^*\|$ bounds the initial distance to a minimizer.

Methodology

The Setup–Complexity Interface

The core methodological innovation is the formalization of optimization problems in Lean 4 through a Setup structure. The framework defines:

1. Params: All problem parameters (Hilbert space $E$, smoothness constant $L$, starting point $x_0$, distance bound $R$, accuracy $\varepsilon$)
2. Public: Only the parameters available to the algorithm (e.g., $E$, $L$, $x_0$ — but not $\varepsilon$ or $R$)
3. Instance/Query/Reply/Output: Types specifying the objective function, oracle interface, and output format
4. valid: Assumptions on parameters (e.g., $L > 0$, $R \geq 0$, $\varepsilon > 0$)
5. admissible: Assumptions on the objective and oracle (convexity, exact gradients, L-smoothness, existence of minimizer)
6. successful: The accuracy criterion (e.g., $f(x_{out}) - f(x^*) \leq \varepsilon$ almost surely)

Convergence Verification

The central verification mechanism is the Convergence proposition:

def Convergence Setup budget : Prop :=
    ∃ makeAlgorithm,
    ∀ p, Setup.valid p →
    ∀ I oracle, Setup.admissible p I oracle →
    let A := makeAlgorithm (Setup.publicInput p)
    let result := execute oracle A (budget p)
    Setup.successful p I result

The quantifier order is crucial: the algorithm constructor is chosen before the hidden instance and oracle, preventing it from adapting to unknown objectives or minimizers.

Agentic Research Pipeline

The research objective is formalized as:

minimize budget
subject to Convergence Setup budget proved in Lean 4.

The authors employ two agents (researcher and reviewer) using Codex and Claude Code. The researcher produces results; the reviewer verifies and decides acceptance. They interact until the reviewer accepts a new research result.

Empirical Validation / Results

The framework produced more than 100 new results, with several highlighted in the paper:

Generalized Smooth Convex Optimization

Under the generalized smoothness assumption $\|\nabla^2 f(x)\| \leq L_0 + L_1\|\nabla f(x)\|$, previous bounds were:

$$\widetilde{\mathcal{O}}\left(1 + \sqrt{\frac{L_0 R^2}{\varepsilon}} + L_1 R\right) \quad \text{and} \quad \widetilde{\mathcal{O}}\left((1+\nu)\left[1 + \sqrt{\frac{L_0 R^2}{\varepsilon}} + (L_1 R)^{2/3}\right]\right)$$

LongTails obtained:

$$\widetilde{\mathcal{O}}\left(1 + \sqrt{\frac{L_0 R^2}{\varepsilon}} + (L_1 R)^{2/3}\right)$$

using only gradient queries, improving the $L_1 R$ term to $(L_1 R)^{2/3}$ and removing the exact line-search cost.

Key Results Summary

Novel Algorithmic Ideas

The agents discovered a non-trivial method for generalized smooth optimization combining acceleration with local curvature estimation: at iteration $k$, the method uses curvature estimate $G_k$ to choose acceleration weight $a_k$, computes gradient $g^k = \nabla f(y^k)$, sets $M_k = 4(L_0 + L_1\|g^k\|)$, and takes gradient step $v^k = y^k - g^k/M_k$. If $M_k > G_k$, the update is damped by $\gamma_k = G_k/M_k$; otherwise, the full update is taken. The analysis separates iterations with low and high local curvature.

Theoretical and Practical Implications

Theoretical Significance

The framework demonstrates that automated discovery of non-trivial mathematical results in optimization is feasible at scale. The obtained results are not merely re-derivations of known bounds but include genuinely novel algorithmic ideas (e.g., the combined acceleration-curvature-estimation method) that improve upon state-of-the-art human-derived bounds.

Practical Implications

1. Scalability: The same formal Lean 4 interface works across diverse optimization problems, allowing repeated improvement of guarantees within each Setup.
2. Verification: All accepted Complexities are formally verified, eliminating the risk of incorrect proofs.
3. Research workflow: The Setup–Complexity abstraction reduces research to a well-defined optimization problem, amenable to agentic search.

Limitations Acknowledged

The authors note that unlike traditional papers, results are not presented individually in separate publications:

"One limitation of this work is that we do not present each result in a separate paper. Although many of these results arguably warrant individual publications in the optimization community, preparing and reviewing on the order of 100 separate papers is infeasible."

Conclusion

LongTails represents a significant step toward scaling automated mathematical research in optimization. The framework's key contributions are:

1. A reusable formal specification in Lean 4 tailored to optimization problems
2. Explicit oracle accounting that makes complexity bounds machine-checkable
3. An agentic research workflow that scales across a broad collection of numerical problems

The framework has already produced more than 100 new theoretical guarantees, with improvements spanning generalized smoothness, heavy-tailed noise, composite optimization, higher-order methods, and monotone operator problems. The authors suggest that as automated discovery scales, the community may need to discuss higher thresholds for standalone publications or alternative ways of presenting and evaluating theoretical results.

Future directions include expanding the collection of Setups, improving existing Complexities, and further developing the framework's capabilities.