Pith. sign in

REVIEW 3 major objections 4 minor 89 references

A Domain-Specific Harness for End-to-End Automation of Optimization Research

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A four-stage automated pipeline—numerical search, LLM discovery, Lean verification, human write-up—produces two new first-order optimization methods with machine-checked convergence theorems.

desk verdict Solid new methods with machine-checked proofs; trim the unproven 'optimal for all N' claim and this is a clean, citable paper. read the letter →

arxiv 2608.07407 v1 pith:P3DESVHT submitted 2026-08-07 math.OC

Heechang Kim , Ernest K. Ryu , Shuvomoy Das Gupta This is my paper · ORCID
classification math.OC MSC 90C2590C2265K0568V20
keywords first-orderoptimizationperformanceestimationprogrammingbranch-and-boundlemniscateaccelerationgradientnormminimizationstronglyconvexLeanformalverificationLLM-assistedmathematicaldiscovery
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that the full loop of optimization research can be automated: numerically searching for the best fixed-step first-order method, discovering a closed-form description of it and a convergence proof with the help of large language models, and machine-checking that proof in the Lean proof assistant. The demonstration consists of two new methods. Lemniscate acceleration minimizes the squared gradient norm of an $L$-smooth convex function at the optimal $O(1/N^4)$ rate, with a constant set by the lemniscate constant $\varpi \approx 2.622$; analytic ITEM-f contracts the function-value gap of a $\mu$-strongly convex function by $(1-\sqrt{\mu/L})^{2}$ per step. The paper reports that both convergence theorems, their supporting lemmas, and the continuous-time analogue of the first are formalized in Lean with no `sorry`, `axiom`, `admit`, or `unsafe` in the development. If correct, the contribution is not only two algorithms but evidence that the bottleneck in this kind of research can move from proof-writing to problem choice and interpretation.

What carries the argument

The load-bearing object is the BnB-PEP collapse of the minimax design problem into a nonconvex QCQP whose feasible points are pairs consisting of a stepsize array and a dual certificate; by weak duality, any feasible dual point is itself a proof of a worst-case bound, so the pipeline can read a Lyapunov proof directly off the certificate’s multipliers. For lemniscate acceleration, the coefficients come from the recurrence $\Omega_N(\rho_k-\rho_{k+1})^2 = \rho_k(1-\rho_{k+1}^2)$ with $1=\rho_0>\cdots>\rho_{N+1}=0$, whose mirror involution $T(\rho)=(1-\rho)/(1+\rho)$ gives the middle coefficient $\sqrt{2}-1$ for odd $N$ and leads to the lemniscate constant in the rate. For ITEM-f, the coefficients come from a planar circle construction with the same flavor of symmetry, $a_k a_{N+1-k}=1$, and that symmetry supplies the identities that make the Lyapunov decrement nonnegative. The Lean formalization turns these Lyapunov identities into checked theorem declarations, so the machinery is what converts numerical patterns into rigorous mathematics.

What would settle it

Rebuild the two published Lean projects with the pinned Lean 4.32.0 and mathlib toolchain, run the stated hygiene scan and axiom audit, and inspect the comparator replay: identifying any `sorry`, `admit`, `unsafe`, or any axiom beyond `propext`, `Quot.sound`, and `Classical.choice` in the closure of the public theorem declarations would falsify the formal-verification claim.

Watch

Extended reading notes

Core claim

On the paper’s own terms, the central discovery is a pair of convergence theorems. Theorem 1 states that for an $L$-smooth convex $f$ with minimizer $x_\star$, the final iterate of lemniscate acceleration satisfies $\|\nabla f(x_N)\|^2 \le L^2\|x_0-x_\star\|^2/\Omega_N^2 \le \varpi^4 L^2\|x_0-x_\star\|^2/(N+1)^4$; Theorem 3 states that for $L$-smooth, $\mu$-strongly convex $f$, analytic ITEM-f satisfies $f(x_N)-f_\star \le (1/\Upsilon_N^2)(f(x_0)-f_\star)\le 4(1-\sqrt{\mu/L})^{2N}(f(x_0)-f_\star)$. The coefficients of both methods are generated by one-dimensional recursions with an involution symmetry, and the proofs run through Lyapunov sequences whose decrements are explicit nonnegative combinations of interpolation inequalities. The paper also reports that the statements are machine-checked in Lean 4.32.0 with mathlib, with an axiom audit limited to `propext`, `Quot.sound`, and `Classical.choice`, and records self-H-duality of both methods as an unformalized observation.

Load-bearing premise

The label “optimal fixed-step method” for LemniAcc and ITEM-f rests on numerical branch-and-bound certificates that are globally certified only for $N=1,\dots,5$ and locally optimal for $N=6,\dots,25$, with no theorem proving global optimality for arbitrary $N$; the printed convergence-rate theorems do not depend on this numerical support.

Editorial extensions

If this is right

  • LemniAcc matches the optimal $O(1/N^4)$ dependence for gradient-norm minimization in smooth convex optimization as a single method, instead of concatenating two different methods, and improves the leading constant by roughly a factor of 1.35 over the chained OGM/OGM-G baseline.
  • Analytic ITEM-f supplies closed-form coefficients for every horizon $N$ and every $0<\mu<L$, replacing the numerically tabulated stepsizes that were previously available only for $N\le 5$.
  • The rate theorems can be cited as machine-checked facts, with the formal statements pinned by the Lean project’s public declarations and axiom audit.
  • The fractional contraction $(1-\sqrt{\mu/L})^{2}$ matches the asymptotic oracle-complexity lower bound for smooth strongly convex minimization.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The optimality claim for every horizon is the part most worth checking next: certified global optimality currently covers only $N=1,\dots,5$, so a proof that the recurrence or circle construction is globally minimax-optimal for all $N$ would convert a numerical label into a theorem.
  • The appearance of the lemniscate constant hints at a broader family of elliptic acceleration methods; one testable extension is to run the same pipeline with other performance measures and see whether other elliptic or algebraic-curve constants appear.
  • If the pipeline generalizes to problem classes the paper explicitly excludes, such as stochastic or second-order methods, then formal verification could become the standard bottleneck-check for computer-assisted algorithm discovery rather than a one-off exercise.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. This paper presents AutoOPT, a four-stage pipeline (BnB-PEP numerical design, LLM-based symbolic discovery, Lean 4 formal verification, and human write-up) for automating parts of first-order optimization research. The two case studies are lemniscate acceleration for reducing the gradient norm of an L-smooth convex function, with the bound ||grad f(x_N)||^2 <= L^2 ||x0-x*||^2 / Omega_N^2 <= varpi^4 L^2 ||x0-x*||^2 / (N+1)^4, and an analytic description of ITEM-f for L-smooth, mu-strongly convex problems with f(x_N)-f* <= (1/Upsilon_N^2)(f(x0)-f*) <= 4(1-sqrt(mu/L))^(2N)(f(x0)-f*). Theorems 1 and 3, their supporting lemmas, the continuous-time LenmiAcc result, and the ITEM-f coefficient construction are reported as formalized in Lean 4.32.0 with mathlib, with no sorry, axiom, admit, or unsafe in the development and with comparator replay on two systems. The paper additionally claims that LemniAcc and analytic ITEM-f are the optimal fixed-step first-order methods for their respective criteria.

Significance. The reported formalization is the strongest part of the paper: if the Lean projects and their axiom audit are as described, Theorems 1 and 3, the supporting Lyapunov lemmas, and the continuous-time result are backed by machine-checked proofs, a standard of evidence that is unusual and valuable. The mathematical content is also of independent interest, particularly LemniAcc as a single method achieving the optimal O(1/N^4) gradient-norm rate with an explicit lemniscate-constant bound, and the first analytic coefficient construction for ITEM-f. The constant comparison with concatenated OGM/OGM-G is plausible. The significance is reduced by the fact that the paper's headline 'optimal method' designation is not proved for arbitrary N: the convergence theorems are one-sided upper bounds, and the optimality certificates are numerical with global certification only for N=1,...,5. The algorithms and their proven rates stand without that claim, but the framing needs correction.

major comments (3)
  1. [Secs. 1.1, 4.1.2, 4.2.2] The claim that LemniAcc and analytic ITEM-f are the optimal fixed-step first-order methods is not supported by any theorem for arbitrary N. Theorems 1 and 3 prove upper bounds on the worst-case quantities, but not a matching analytic minimax lower bound with the constants Omega_N and Upsilon_N. The BnB-PEP certificates described in Sections 4.1.2 and 4.2.2 certify global optimality only for N=1,...,5, with N=6,...,25 locally optimal, and the Lean projects formalize the convergence theorems, not an optimality theorem. Since 'optimal' is a headline claim in the abstract, Section 1.1, and the two design subsections, this is a load-bearing gap. The correct wording would be to present the methods as having proven rates and constants, with numerical certification of optimality at short horizons, or to supply an analytical minimax lower bound.
  2. [Sec. 4.1.2 and Sec. 4.2.2] The design subsections state that AutoOPT 'jointly searches over the coefficients and a convergence certificate to minimize C_N' and that ITEM-f 'attains the optimal value C_N = 1/Upsilon_N^2'. This conflates the analytic feasible point of an inner dual (which certifies an upper bound by weak duality) with a proof of optimality. A feasible dual point proves that a method has a worst-case guarantee at least as good as the bound; it does not prove that no other FSFOM has a better guarantee. Because no converse certificate or analytic lower-bound construction is given, the optimality assertion should be explicitly labeled as numerical evidence for small horizons, consistent with the calibrated-evidence standard advocated in Section 3.4.
  3. [Sec. 4.2, Theorem 3] The presentation of the ITEM-f rate should distinguish the exact contraction factor 1/Upsilon_N^2 from the asymptotic rate (1-sqrt(mu/L))^{2N}. Theorem 3 proves the second inequality via Lemma 18, which contains an extra factor 4; the abstract and Section 4.2.2 describe the per-step factor (1-sqrt(mu/L))^2 as if it were the exact contraction factor. This is a presentation issue rather than a mathematical error, but it contributes to the paper's overstatement of what has been proved about ITEM-f.
minor comments (4)
  1. [Sec. 3.4] The paper explicitly calls for a calibrated standard of evidence in which each claim receives an evidentiary label, but the 'optimal' claims in Sections 1.1, 4.1.2, and 4.2.2 do not carry such a label. Adding 'numerically certified for N<=5, local for N=6,...,25, unproved for general N' would make the paper consistent with its own methodological principle.
  2. [Sec. 4.2.3] In the paragraph beginning 'We note the continuous-time limit', the notation L = N^2/T^2 is used before the scaling of the discrete method is fully explained; a sentence stating that this is the algorithmic smoothness bound used in the N-to-continuous limit would improve readability.
  3. [Sec. 4.3] Remark 2 records self-H-duality without proof or Lean verification, while the section title presents it as a finding. Since the remark itself says it is an observation, the title could be softened to 'Observed self-H-duality' to match the evidentiary status.
  4. [Appendix A.1] The proof of Lemma 8 and several places in the appendices refer to 'tedious but straightforward algebra' or 'tedious but straightforward' manipulations. These are acceptable in a paper with a Lean formalization, but a short symbolic-check note or a reference to the Lean files for those identities would aid readers who do not wish to redo the algebra.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the convergence theorems are proven from independently defined coefficient constructions and machine-checked in Lean; the numerical optimality extrapolation is an evidence-level issue, not a definitional loop.

full rationale

The derivation chain is not circular. Theorem 1 and Theorem 3 do not assume their target inequalities. LemniAcc's coefficients are fixed by Lemma 1, which proves existence and uniqueness of Ω_N and ρ_k from the recurrence Ω_N(ρ_k−ρ_{k+1})^2 = ρ_k(1−ρ_{k+1}^2), with no reference to the gradient-norm bound; Theorem 1 then derives the bound through the Lyapunov sequence (11) and the nonnegative decomposition (13). Similarly, ITEM-f's coefficients are fixed by the geometric construction of Lemma 4, whose existence and uniqueness are proved by the shooting argument in Appendix B.1, and the bound in Theorem 3 follows from endpoint comparisons and the monotonicity of Lemma 6. The Lean formalization in Sections 4.1.5 and 4.2.4 independently checks these proofs; the axiom audit and comparator replay are machine-verification evidence, not self-citation. The fact that the analytic formulas were discovered by fitting numerical BnB-PEP solutions and LLM consultation concerns provenance, not logical circularity: the proof obligations are discharged by explicit verification after discovery, and the constants are not defined in terms of the target bounds. The only advertised property not proven for arbitrary N is exact minimax optimality of the two methods: Section 4.1.2 states that global certificates cover N = 1,...,5 and local optimality N = 6,...,25, and the extrapolation to all N is numerical, not theorem-based. That is a calibration and evidence concern, as the paper itself urges in Section 3.4, not a circular reduction; neither Theorem 1 nor Theorem 3 relies on the optimality extrapolation. The unformalized remarks, Remark 1 and Remark 2, are explicitly flagged in the text as not machine-checked, so they are not presented as derived from the formalized theorems.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The final theorems rest on standard smooth-convex interpolation facts, explicitly stated coefficient constructions, and standard Lean axioms. No fitted free parameters appear in the theorem statements; Omega_N and Upsilon_N are unique solutions of stated recurrences and geometric constraints. The design-stage optimality claims additionally assume strong duality and large dimension, both disclosed in the text.

assumptions (5)
  • domain assumption Smooth convex functions satisfy the interpolation inequality f(x)-f(y)-<grad f(y),x-y>-(1/(2L))||grad f(x)-grad f(y)||^2 >= 0.
    Invoked at the start of Section 4.1.1 as equation (6) and formalized as finite_interpolation in Lean. Every Lyapunov decrement and terminal decomposition uses this inequality.
  • domain assumption The finite smooth-convex interpolation characterization is lossless for the PEP reduction.
    Used in Section 3.1 and Appendix A.3 to replace the infinite-dimensional function class with sampled constraints, relying on Taylor, Hendrickx, and Glineur. This is a standard external theorem.
  • domain assumption Strong duality holds between the inner SDP and its dual.
    Assumption 2 in Section 3.1 and used in the BnB-PEP design derivation. It supports the numerical optimality interpretation, not the final Lyapunov theorems.
  • domain assumption Large-scale dimension condition d >= N+2.
    Assumption 1 in Appendix A.3, used to drop the rank constraint in the Gram lifting. The paper states this explicitly.
  • standard math Standard Lean axioms propext, Quot.sound, and Classical.choice.
    The reported axiom audit attributes exactly these to every public declaration. These are foundational axioms of the Lean/mathlib system.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Domain-Specific Harness for End-to-End Automation of Optimization Research." pith.science (2026). https://pith.science/paper/P3DESVHT

@misc{pith2026260807407,
  author       = {Pith},
  title        = {Pith review of: A Domain-Specific Harness for End-to-End Automation of Optimization Research},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/P3DESVHT}},
  note         = {Machine review of arXiv:2608.07407}
}
abstract

We present AutoOPT, a domain-specific harness for end-to-end automation of optimization research. AutoOPT organizes the discovery of optimal first-order methods into four stages: numerical design through the BnB-PEP methodology; symbolic discovery of the analytic description and a convergence proof through frontier large language models (LLMs); formal verification in the Lean 4 proof assistant; and human interpretation and write-up. We demonstrate the framework on two case studies, each of independent interest. The first, lemniscate acceleration, is a new accelerated gradient method for minimizing the gradient norm of a smooth convex function: after $N$ gradient steps it reduces the squared gradient norm at the optimal $O(1/N^{4})$ rate, with a constant governed by the lemniscate constant $\varpi$, a classical elliptic-integral constant. The second is the analytic description of ITEM-f, a method previously known only numerically: for $L$-smooth, $\mu$-strongly convex minimization it contracts the function-value gap at an accelerated linear rate with a per-step factor $(1-\sqrt{\mu/L})^{2}$. The convergence theorems of both case studies are formalized and machine-checked in Lean 4.

Figures

Figures reproduced from arXiv: 2608.07407 by the authors.

Figure 1
Figure 1. The researcher operates AutoOPT by conversing with an LLM agent in a research workspace in four stages. Stage 1 numerically designs an optimal first-order method for the problem class that the researcher specifies. Stage 2 consults a frontier LLM to propose an analytic form of the numerically designed method along with candidate convergence proofs. Stage 3 formally verifies the candidate theorems and proofs in the L… view at source ↗
Figure 2
Figure 2. Stage 1 of AutoOPT. Numerical design of the optimal method via bnb-pep-skill. 3.2 Stage 2: Symbolic discovery of analytic descriptions and convergence proofs via LLMs Numerical to symbolic discovery. Once the numerically optimal stepsizes and the BnB-PEP mathematical derivation are available from Stage 1, AutoOPT invokes the skill frontier-llm-consult to discover analytic descriptions of the numerically designed met… view at source ↗
Figure 4
Figure 4. An illustrative Stage-2 prompt sequence for the lemniscate case study: one initial prompt followed by two follow-up prompts corresponding to the three substeps of Section 3.2 [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figures from the paper (8 more)
Figure 3
Figure 3. Figure 3: Stage 2 of AutoOPT. Symbolic discovery of analytic descriptions of the numerically designed methods and their candidate convergence proofs via frontier-llm-consult. Preparation for machine verification. At the end of this stage, AutoOPT saves the outputs from the front…
Figure 5
Figure 5. Figure 5: Formal verification via lean-verify: candidate theorems and proofs from Stage 2 are formalized in Lean, checked by Lean itself, and re-examined by an independent verifier; the result is recorded as formally verified only after the human authors confirm that the formal …
Figure 6
Figure 6. Figure 6: The unit lemniscate (x 2 + y 2 ) 2 = x 2 − y 2 with foci at (±1/ √ 2, 0) and tips at (±1, 0). Its perimeter is 2ϖ, and its diameter is 2. Thus ϖ ≈ 2.62206 is its perimeter-to-diameter ratio. The lemniscate elliptic functions are defined through the arc-length integral …
Figure 7
Figure 7. Figure 7: Continuous-time coefficient profiles. The left panel shows ρ(t) = cl2 (ϖt/(2T)) together with the discrete coefficients ρk for N = 40, placed at tk = k T /(N + 1). We see that ρ(t) is the continuous limit of the discrete coefficients. The right panels show σ(t) = p 1/ρ…
Figure 8
Figure 8. Figure 8: An illustrative Stage-3 prompt for the formal verification of the lemniscate accelerated gradient method using the lean-verify skill. Public theorem declarations 10 Dependency nodes in the closure 22 Lean source files 22 Lines of Lean 7,384 lake build jobs, native macO…
Figure 9
Figure 9. Figure 9: File structure of the Lean project for the lemniscate accelerated gradient method (module files grouped by folder). The wrappers Challenge.lean, Solution.lean, and config.json pin the ten public theorems and the permitted axioms for the comparator, and artifacts/ recor…
Figure 10
Figure 10. Figure 10: The planar construction underlying Lemma 4, shown for N = 3, q = 0.1. The inter￾mediate points P1, . . . , PN (◦) lie on the circle of radius RN = p Υ2 N − 1 centered at C = (ΥN , 0); the endpoints P0 and PN+1 () lie strictly inside; successive points satisfy (Pk − C…
Figure 11
Figure 11. Figure 11: File structure of the ITEM-f Lean project (module files grouped by folder). The proof-free Spec/ layer is all that Challenge.lean imports, so the proofs reach the comparator only through Solution.lean; config.json pins the fourteen public theorems and the permitted ax…

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

89 extracted references · 43 canonical work pages

  1. [1]

    Agent Skills overview, 2026

    Agent Skills. Agent Skills overview, 2026. URL: https://agentskills.io/home [cited 2026-08-03]

    2026

  2. [2]

    Altschuler and Pablo A

    Jason M. Altschuler and Pablo A. Parrilo. Acceleration by stepsize hedging: Multi-Step Descent and the Silver Stepsize Schedule. Journal of the ACM , 72(2):1–38, 2025. doi: 10.1145/3708502

    doi:10.1145/3708502 2025

  3. [3]

    Altschuler and Pablo A

    Jason M. Altschuler and Pablo A. Parrilo. Acceleration by stepsize hedging: Silver Stepsize Schedule for smooth convex optimization. Mathematical Programming, 213(1–2):1105–1118,

  4. [4]

    Altschuler and Pablo A

    Jason M. Altschuler and Pablo A. Parrilo. Stepsize Hedging: An alternative mechanism for accelerating gradient descent, 2026. To appear as an invited Research Highlight in the 2026 INFORMS Computing Society Newsletter. arXiv:2605.31386

    arXiv 2026

  5. [5]

    Claude Code overview, 2026

    Anthropic. Claude Code overview, 2026. URL: https://code.claude.com/docs/en/overvi ew [cited 2026-08-03]

    2026

  6. [6]

    Extend Claude with skills, 2026

    Anthropic. Extend Claude with skills, 2026. URL: https://code.claude.com/docs/en/sk ills [cited 2026-08-03]

    2026

  7. [7]

    Artelys Knitro, 2026

    Artelys. Artelys Knitro, 2026. URL: https://www.artelys.com/solvers/knitro/ [cited 2026-08-03]

    2026

  8. [8]

    Accurate prediction of protein structures and interactions using a three-track neural network

    Minkyung Baek, Frank DiMaio, Ivan Anishchenko, Justas Dauparas, Sergey Ovchinnikov, et al. Accurate prediction of protein structures and interactions using a three-track neural network. Science, 373(6557):871–876, 2021. doi:10.1126/science.abj8754

    doi:10.1126/science.abj8754 2021

Show all 89 references
  1. [9]

    Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. Julia: A fresh approach to numerical computing. SIAM Review , 59(1):65–98, 2017. doi:10.1137/141000671

    2017 doi

  2. [10]

    Byrd, Jorge Nocedal, and Richard A

    Richard H. Byrd, Jorge Nocedal, and Richard A. Waltz. KNITRO: An integrated package for nonlinear optimization. In Gianni di Pillo and Massimo Roma, editors, Large-Scale Non- linear Optimization, volume 83 of Nonconvex Optimization and Its Applications , pages 35–59. Springer,...

    2006 doi

  3. [11]

    Xiangning Chen, Chen Liang, Da Huang, Esteban Real, Kaiyuan Wang, Hieu Pham, Xuanyi Dong, Thang Luong, Cho-Jui Hsieh, Yifeng Lu, and Quoc V. Le. Symbolic discovery of 37 optimization algorithms. In Advances in Neural Information Processing Systems , volume 36, pages 49205–4923...

    2023 doi

  4. [12]

    Ipopt license, 2026

    COIN-OR. Ipopt license, 2026. URL: https://coin-or.github.io/Ipopt/LICENSE.html [cited 2026-08-03]

    2026

  5. [13]

    Research highlight: A tutorial on branch-and-bound performance estimation programming

    Shuvomoy Das Gupta. Research highlight: A tutorial on branch-and-bound performance estimation programming. INFORMS Computing Society Newsletter , pages 15–28, May 2025. URL: https://higherlogicdownload.s3.amazonaws.com/INFORMS/a4f852dd-2bdc-46b c-98e7-47e7d7c12752/UploadedImag...

    2025

  6. [14]

    Shuvomoy Das Gupta, Bart P. G. Van Parys, and Ernest K. Ryu. Branch-and-bound perfor- mance estimation programming: A unified methodology for constructing optimal optimization methods. Mathematical Programming, 204(1–2):567–639, 2024. doi:10.1007/s10107-023-0 1973-1

    2024 doi

  7. [15]

    Alexandre d’Aspremont, Damien Scieur, and Adrien B. Taylor. Acceleration methods. Foun- dations and Trends ® in Optimization , 5(1–2):1–245, 2021. doi:10.1561/2400000036

    2021 doi

  8. [16]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28 , volume 12699 of Lecture Notes in Computer Science, pages 625–635. Springer, 2021. doi:10.1007/978-3-030-79876-5_37

    2021 doi

  9. [17]

    The exact information-based complexity of smooth convex minimization

    Yoel Drori. The exact information-based complexity of smooth convex minimization. Journal of Complexity , 39:1–16, 2017. doi:10.1016/j.jco.2016.11.001

    2017 doi

  10. [18]

    Yoel Drori and Adrien B. Taylor. On the oracle complexity of smooth strongly convex mini- mization. Journal of Complexity , 68:101590, 2022. doi:10.1016/j.jco.2021.101590

    2022

  11. [19]

    Performance of first-order methods for smooth convex min- imization: A novel approach

    Yoel Drori and Marc Teboulle. Performance of first-order methods for smooth convex min- imization: A novel approach. Mathematical Programming , 145(1–2):451–482, 2014. doi: 10.1007/s10107-013-0653-0

    2014 doi

  12. [20]

    Alhussein Fawzi, Matej Balog, Aja Huang, Thomas Hubert, Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Francisco J. R. Ruiz, Julian Schrittwieser, Grzegorz Swirszcz, David Silver, Demis Hassabis, and Pushmeet Kohli. Discovering faster matrix multiplicat...

    2022 doi

  13. [21]

    Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N

    Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao...

    2026

  14. [22]

    Hendrickx, Adrien B

    Baptiste Goujaud, Céline Moucer, François Glineur, Julien M. Hendrickx, Adrien B. Taylor, and Aymeric Dieuleveut. PEPit: computer-assisted worst-case analyses of first-order opti- mization methods in Python. Mathematical Programming Computation , 16(3):337–367, 2024. doi:10.10...

    2024 doi

  15. [23]

    Provably faster gradient descent via long steps

    Benjamin Grimmer. Provably faster gradient descent via long steps. SIAM Journal on Opti- mization, 34(3):2588–2608, 2024. doi:10.1137/23M1588408

    2024 doi

  16. [24]

    Gurobi academic licenses, 2026

    Gurobi Optimization, LLC. Gurobi academic licenses, 2026. URL: https://www.gurobi.com /academics [cited 2026-08-03]

    2026

  17. [25]

    Gurobi Optimizer Reference Manual, version 13.0, 2026

    Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, version 13.0, 2026. URL: https://docs.gurobi.com/projects/optimizer/en/current/ [cited 2026-08-03]

    2026

  18. [26]

    Horn and Charles R

    Roger A. Horn and Charles R. Johnson. Matrix Analysis . Cambridge University Press, 2nd edition, 2012. doi:10.1017/CBO9781139020411

    2012 doi

  19. [27]

    Uijeong Jang, Shuvomoy Das Gupta, and Ernest K. Ryu. Computer-assisted design of ac- celerated composite optimization methods: OptISTA. Mathematical Programming , 2025. doi:10.1007/s10107-025-02258-5

    2025 doi

  20. [28]

    Highly accurate protein structure prediction with AlphaFold

    John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ron- neberger, et al. Highly accurate protein structure prediction with AlphaFold. Nature, 596(7873):583–589, 2021. doi:10.1038/s41586-021-03819-2

    2021 doi

  21. [29]

    Closing the oracle-complexity gap in derivative-free convex optimization: A near-quadratic lower bound from exact function values, 2026

    Phillip Kerger. Closing the oracle-complexity gap in derivative-free convex optimization: A near-quadratic lower bound from exact function values, 2026. arXiv:2607.13335

    2026 arXiv

  22. [30]

    Donghwan Kim and Jeffrey A. Fessler. Optimized first-order methods for smooth convex minimization. Mathematical Programming, 159(1-2):81–107, 2016. doi:10.1007/s10107-015 -0949-3

    2016 doi

  23. [31]

    Donghwan Kim and Jeffrey A. Fessler. Optimizing the efficiency of first-order methods for decreasing the gradient of smooth convex functions. Journal of Optimization Theory and Applications, 188(1):192–219, 2021. doi:10.1007/s10957-020-01770-2

    2021 doi

  24. [32]

    Jaeyeon Kim, Asuman Ozdaglar, Chanwoo Park, and Ernest K. Ryu. Time-reversed dissipation induces duality between minimizing gradient norm and function value. Advances in Neural Information Processing Systems , 36:23389–23440, 2023. doi:10.52202/075280-1014

    2023 doi

  25. [33]

    Jaeyeon Kim, Chanwoo Park, Asuman Ozdaglar, Jelena Diakonikolas, and Ernest K. Ryu. Mirror duality in convex optimization, 2023. arXiv:2311.17296

    2023 arXiv

  26. [34]

    The AI scientist: Towards fully automated open-ended scientific discovery, 2024

    Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune, and David Ha. The AI scientist: Towards fully automated open-ended scientific discovery, 2024. arXiv:2408.06292

    2024 arXiv

  27. [35]

    Towards end-to-end automation of AI research

    Chris Lu, Cong Lu, Robert Tjarko Lange, Yutaro Yamada, Shengran Hu, Jakob Foer- ster, David Ha, and Jeff Clune. Towards end-to-end automation of AI research. Nature, 651(8107):914–919, 2026. doi:10.1038/s41586-026-10265-5

    2026 doi

  28. [36]

    JuMP 1.0: Recent improvements to a modeling language for math- ematical optimization

    Miles Lubin, Oscar Dowson, Joaquim Dias Garcia, Joey Huchette, Benoît Legat, and Juan Pablo Vielma. JuMP 1.0: Recent improvements to a modeling language for math- ematical optimization. Mathematical Programming Computation , 15:581–589, 2023. doi: 10.1007/s12532-023-00239-3 . 39

    2023 doi

  29. [37]

    Convergence of BDRS as a matrix scaling algorithm

    Shiqian Ma. Convergence of BDRS as a matrix scaling algorithm. Optimization Online preprint, 2026. URL: https://optimization- online.org/2026/05/convergence- o f-bdrs-as-a-matrix-scaling-algorithm/

    2026

  30. [38]

    MOSEK academic licenses, 2026

    MOSEK ApS. MOSEK academic licenses, 2026. URL: https://www.mosek.com/products /academic-licenses/ [cited 2026-08-03]

    2026

  31. [39]

    The MOSEK optimizer API for Julia 11.2.2, 2026

    MOSEK ApS. The MOSEK optimizer API for Julia 11.2.2, 2026. URL: https://docs.mos ek.com/latest/juliaapi/index.html [cited 2026-08-03]

    2026

  32. [40]

    Nemirovsky

    Arkadi S. Nemirovsky. On optimality of Krylov’s information when solving linear operator equations. Journal of Complexity , 7(2):121–130, 1991. doi:10.1016/0885-064X(91)90001-E

    1991 doi

  33. [41]

    Nemirovsky

    Arkadi S. Nemirovsky. Information-based complexity of linear operator equations. Journal of Complexity, 8(2):153–175, 1992. doi:10.1016/0885-064X(92)90013-2

    1992 doi

  34. [42]

    Nemirovsky and David B

    Arkadi S. Nemirovsky and David B. Yudin. Problem Complexity and Method Efficiency in Optimization. Wiley, 1983

    1983

  35. [43]

    A method of solving a convex programming problem with convergence rate O(1/k2)

    Yurii Nesterov. A method of solving a convex programming problem with convergence rate O(1/k2). Soviet Mathematics Doklady , 27(2):372–376, 1983

    1983

  36. [44]

    Primal-dual accelerated gradient methods with small-dimensional relaxation oracle

    Yurii Nesterov, Alexander Gasnikov, Sergey Guminov, and Pavel Dvurechensky. Primal-dual accelerated gradient methods with small-dimensional relaxation oracle. Optimization Methods and Software , 36(4):773–810, 2021. doi:10.1080/10556788.2020.1731747

    2021

  37. [45]

    Hermes Agent, 2026

    Nous Research. Hermes Agent, 2026. URL: https://hermes-agent.nousresearch.com/ [cited 2026-08-03]

    2026

  38. [46]

    Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushme...

    2025 arXiv

  39. [47]

    Introducing ChatGPT Pro, 2024

    OpenAI. Introducing ChatGPT Pro, 2024. URL: https://openai.com/index/introducing -chatgpt-pro/ [cited 2026-08-03]

    2024

  40. [48]

    Build skills, 2026

    OpenAI. Build skills, 2026. URL: https://learn.chatgpt.com/docs/build-skills [cited 2026-08-03]

    2026

  41. [49]

    Codex CLI, 2026

    OpenAI. Codex CLI, 2026. URL: https://developers.openai.com/codex/cli [cited 2026-08-03]

    2026

  42. [50]

    GPT-5.6: Frontier intelligence that scales with your ambition, 2026

    OpenAI. GPT-5.6: Frontier intelligence that scales with your ambition, 2026. URL: https: //openai.com/index/gpt-5-6/ [cited 2026-08-03]

    2026

  43. [51]

    Introducing GPT-5.5, 2026

    OpenAI. Introducing GPT-5.5, 2026. URL: https://openai.com/index/introducing-gpt -5-5/ [cited 2026-08-03]

    2026

  44. [52]

    Ten advances in mathematics and theoretical computer science, 2026

    OpenAI. Ten advances in mathematics and theoretical computer science, 2026. URL: https: //cdn.openai.com/pdf/ten-proofs-oai.pdf [cited 2026-08-03]. 40

    2026

  45. [53]

    OpenClaw docs, 2026

    OpenClaw Foundation. OpenClaw docs, 2026. URL: https://docs.openclaw.ai/ [cited 2026-08-03]

    2026

  46. [54]

    OpenCode: The open source AI coding agent, 2026

    OpenCode. OpenCode: The open source AI coding agent, 2026. URL: https://opencode.ai/ [cited 2026-08-03]

    2026

  47. [55]

    Pawan Kumar, Emilien Dupont, Francisco J

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with larg...

    2024

  48. [56]

    Hendrickx

    Anne Rubbens and Julien M. Hendrickx. A constraint-based approach to function interpola- tion, with application to performance estimation for weakly convex optimization. Mathematical Programming, 2026. doi:10.1007/s10107-026-02353-1

    2026 doi

  49. [57]

    Hendrickx, and Adrien B

    Anne Rubbens, Julien M. Hendrickx, and Adrien B. Taylor. A constructive approach to strengthen algebraic descriptions of function and operator classes, 2025. arXiv:2504.14377

    2025 arXiv

  50. [58]

    Suh, Gyumin Roh, and Ernest K

    Jaewook J. Suh, Gyumin Roh, and Ernest K. Ryu. Continuous-time analysis of accelerated gradient methods via conservation laws in dilated coordinate systems. In Proceedings of the 39th International Conference on Machine Learning , volume 162 of Proceedings of Machine Learning ...

    2022

  51. [59]

    Suh, TaeHo Yoon, Edward D

    Jaewook J. Suh, TaeHo Yoon, Edward D. H. Nguyen, Bicheng Ying, and Shiqian Ma. Peppy: An AI-assisted workflow for tight convergence analysis of optimization algorithms. In ICML 2026 Workshop AI4Research , 2026. Seoul, South Korea. URL: https://openreview.net/f orum?id=q7TfzOgGnb

    2026

  52. [60]

    Anja Surina, Arun Suggala, George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Francisco J. R. Ruiz, Pushmeet Kohli, and Swarat Chaudhuri. An improved last-iterate convergence rate for anchored gradient descent ascent, 2026. arXiv:2604.03782

    2026 arXiv

  53. [61]

    Bulaong, John E

    Kyle Swanson, Wesley Wu, Nash L. Bulaong, John E. Pak, and James Zou. The Virtual Lab of AI agents designs new SARS-CoV-2 nanobodies. Nature, 646(8085):716–723, 2025. doi:10.1038/s41586-025-09442-9

    2025 doi

  54. [62]

    Taylor and Yoel Drori

    Adrien B. Taylor and Yoel Drori. An optimal gradient method for smooth strongly convex minimization. Mathematical Programming, 199(1–2):557–594, 2023. doi:10.1007/s10107-0 22-01839-y

    2023 doi

  55. [63]

    Taylor, Julien M

    Adrien B. Taylor, Julien M. Hendrickx, and François Glineur. Exact worst-case performance of first-order methods for composite convex optimization. SIAM Journal on Optimization , 27(3):1283–1313, 2017. doi:10.1137/16M108104X

    2017 doi

  56. [64]

    Taylor, Julien M

    Adrien B. Taylor, Julien M. Hendrickx, and François Glineur. Performance estimation toolbox (PESTO): automated worst-case analysis of first-order optimization methods. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , pages 1278–1283. IEEE, 2017. doi: 10.1109...

    2017

  57. [65]

    Taylor, Julien M

    Adrien B. Taylor, Julien M. Hendrickx, and François Glineur. Smooth strongly convex interpo- lation and exact worst-case performance of first-order methods. Mathematical Programming, 161(1–2):307–345, 2017. doi:10.1007/s10107-016-1009-3

    2017 doi

  58. [66]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs , pages 367–381. Association for Computing Machinery, 2020. doi:10.1145/3372885.3373824

    2020

  59. [67]

    Advancing mathematics research with AI-driven formal proof search,

    George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, et al. Advancing mathematics research with AI-driven formal proof search,

  60. [68]

    Manu Upadhyaya, Daniel Berg Thomsen, Aymeric Dieuleveut, and Adrien B. Taylor. An optimal first-order method for smooth and strongly convex composite optimization and its stationary limit, 2026. arXiv:2605.22929

    2026 arXiv

  61. [69]

    Andreas Wächter and Lorenz T. Biegler. On the implementation of an interior-point fil- ter line-search algorithm for large-scale nonlinear programming. Mathematical Programming, 106(1):25–57, 2006. doi:10.1007/s10107-004-0559-y

    2006 doi

  62. [70]

    Elliptic functions and transcendence

    Michel Waldschmidt. Elliptic functions and transcendence. In Krishnaswami Alladi, edi- tor, Surveys in Number Theory , volume 17 of Developments in Mathematics , pages 143–188. Springer, New York, 2008. doi:10.1007/978-0-387-78510-3_7

    2008 doi

  63. [71]

    A theory of composition and duality of extremal optimal fixed-point algorithms, 2026

    TaeHo Yoon and Benjamin Grimmer. A theory of composition and duality of extremal optimal fixed-point algorithms, 2026. arXiv:2605.02231

    2026 arXiv

  64. [72]

    Suh, and Ernest K

    TaeHo Yoon, Jaeyeon Kim, Jaewook J. Suh, and Ernest K. Ryu. Optimal acceleration for minimax and fixed-point problems is not unique. In Proceedings of the 41st International Conference on Machine Learning , volume 235 of Proceedings of Machine Learning Research , pages 57244–5...

    2024

  65. [73]

    Ryu, and Benjamin Grimmer

    TaeHo Yoon, Ernest K. Ryu, and Benjamin Grimmer. H-invariance theory: A complete characterization of minimax optimal fixed-point algorithms, 2025. arXiv:2511.14915

    2025 arXiv

  66. [74]

    The agentic researcher: A practical guide to AI-assisted research in mathematics and machine learning, 2026

    Max Zimmer, Nico Pelleriti, Christophe Roux, and Sebastian Pokutta. The agentic researcher: A practical guide to AI-assisted research in mathematics and machine learning, 2026. arXiv: 2603.15914. A Deferred proofs and details for lemniscate acceleration A.1 Existence and uniqu...

    2026

  67. [76]

    FΩ(ρ) = 0 if and only if Ωρ = 1

  68. [77]

    F is continuous on A and strictly increasing in each of Ω and ρ on the fibers of A (the other variable being fixed). Proof. The quarter-discriminant of the quadratic equals Ω2ρ2(Ω+ρ)(Ωρ2ρ) = ρ2 +Ωρ(1ρ2)> 0, so ( 23) has the two real solutions t± = Ωρ p ρ2 + Ωρ(1ρ2) Ω +ρ . Sinc...

  69. [78]

    For the induction step, assume (ΩN,fΦk(ΩN )g) is admissible for horizon N

    with ρ0 = 1 and ρ1 = 0, that is, Ω0 = 1; and indeed Φ1(1) = F1(1) = 0 . For the induction step, assume (ΩN,fΦk(ΩN )g) is admissible for horizon N . We first record, by induction on k2f 1,...,N + 1g, that the maps Ω7! Φk(Ω) are well defined, continuous, and strictly increasing ...

  70. [79]

    (N + 1)2 ϖ2 < ΩN < (N + 1) 2, where ϖ is the lemniscate constant defined in Theorem 1; moreover 1 = Ω 0< Ω1< Ω2<

  71. [80]

    , computing Φk+1(Ω) = FΩ (Φk(Ω)) whenever Φk(Ω) 1/Ω

    Fix Ω 1 and generate the shooting iterates Φ0(Ω), Φ1(Ω),... , computing Φk+1(Ω) = FΩ (Φk(Ω)) whenever Φk(Ω) 1/Ω. If Ω > ΩN , then Φk(Ω) > 1/Ω for all 0 k N and ΦN +1(Ω)> 0. If Ω< ΩN , then there is an index k N with Φk(Ω)< 1/Ω. If Ω = Ω N , the iterates realize the sequence of...

  72. [81]

    sl is a continuous strictly increasing bijection of [0,ϖ/ 2] onto [0, 1] with sl(0) = 0 and sl(ϖ/2) = 1 ; consequently cl is a continuous strictly decreasing bijection of [0,ϖ/ 2] onto [0, 1], and sl(x), cl(x)2 (0, 1) for x2 (0,ϖ/ 2)

  73. [82]

    sl′(x) = q 1 sl4(x) and cl′(x) = q 1 cl4(x) for x2 (0,ϖ/ 2)

  74. [83]

    cl(ϖ/2x) = sl(x) for x2 [0,ϖ/ 2]

  75. [84]

    cl2(x) = 1 sl2(x) 1 + sl2(x) for x2 [0,ϖ/ 2]; equivalently, cl2(x) + sl2(x) + cl2(x) sl2(x) = 1

  76. [85]

    sl(x) = x +o(x) as x# 0

  77. [86]

    T , we substitute Z =σ3 ˙X/4 and expand the two squared norms in ( 36) to expose the cancellation between potentially singular terms as t

    For T > 0, the coefficient ( 34) satisfies 0 < ρ(t) < 1 for t2 (0,T ). Its symmetry identity ρ(Tt) = (1ρ(t))/ (1 +ρ(t)) holds for t2 [0,T ]. Proof. Part 1. On [0, 1) the integrand 1/ p 1x4 is positive, and near x = 1 it is bounded by 1/p1x, so arcsl is a continuous strictly inc...

  78. [87]

    Fp is well defined on R: the argument of the arccos lies in (1 2q, 1) (1, 1), so Fp(θ)θ2 (0,π )

  79. [88]

    Fp is strictly increasing in θ

  80. [89]

    for fixed θ with cosθ< 0, the map p7!Fp(θ) is strictly decreasing. Proof. Writeu ≜ 1qp cosθ. Claim 1 follows from jp cosθj p < qleading to 1< 1 2q < 1qp u 1q +p< 1. For claim 2, differentiating in θ givesF ′ p(θ) = 1 (p sinθ/ p 1u2), so it suffices to prove p2 sin2θ< 1u2 expand...

  81. [2025]

    doi:10.1007/s10107-024-02164-2

    doi

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.