PaperlayerView exact revision on arXiv

Source-linked AI summary

A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

Chenyi Li, Zhijian Lai, Dong An, Jiang Hu, Zaiwen Wen

arXiv:2512.09443v3cs.HCcs.AImath.OC

TL;DR

Mathematical research requires sustained reasoning and verifiable correctness, while LLMs can assist with mathematical reasoning. The paper presents a human-in-the-loop workflow for refining model suggestions into checked statements and proofs. Its Grover-compatible case study illustrates a PL-based O(√N log(1/ε)) convergence bound under stated conditions.

  • Problem

    Mathematical research demands sustained abstraction, coherence over long arguments, and verifiable correctness, motivating ways to use LLMs while keeping human expertise central.

    Source: §1 · p. 1

  • Method

    The workflow has experts set assumptions and verify model-proposed proofs or contradictions, then refine surviving ideas into precise statements and arguments.

    Source: §1 · p. 1, §5.1.1 · p. 11, §6 · p. 19

  • Results

    O(√N log(1/ε)) is the PL-based complexity bound reported for the Grover-compatible Riemannian gradient method when iterates lie in and remain in the region satisfying the PL and pullback-gradient smoothness bounds.

    Source: §7 · p. 19

  • Takeaways & Limitations

    The workflow documents what models proposed, how suggestions were verified, which routes were rejected or corrected, and which validated statements entered the paper.

    Source: §7 · p. 19

    The workflow presupposes domain experts able to identify shifted assumptions, notation drift, missing arguments, and misuse of standard lemmas.

    Source: §6 · p. 19

Abstract

from arXiv · show

We investigate how large language models can be used as research tools in scientific computing while preserving mathematical rigor. We propose a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs. Human experts retain control over problem formulation and assumptions, while the model searches for proofs or contradictions, proposes candidate properties and theorems, and helps construct structures and parameters that satisfy explicit constraints, supported by numerical experiments and simple verification checks. Experts treat these outputs as raw material, further refine them, and organize the results into precise statements and rigorous proofs. We instantiate this workflow in a main case study on the connection between manifold optimization and Grover's quantum search algorithm, where the pipeline identifies invariant subspaces and explores Grover-compatible retractions. The main case study uses the corresponding Grover-compatible convergence analysis, including an $O(\sqrt{N} \log(1/\varepsilon))$ PL-based bound established in the companion mathematical work, to illustrate the refinement stage of the workflow. Prompt records and reusable templates for implementing the workflow are provided. We further include a multi-oracle case study, document representative failed and corrected routes arising from this setting, and provide a structured failure-mode analysis.

1. Introduction.

The paper proposes a human-in-the-loop workflow that uses LLMs to support mathematical research while keeping experts responsible for scope, validation, and rigorous statements. It introduces the workflow through case studies in Grover-compatible Riemannian optimization and describes how AI can assist topic formulation, fixed-target proving, and theorem discovery.

1. Introduction.

  • Prior AI research spans mathematical discovery, Olympiad proving, scientific workflows, and writing, while mathematical rigor still requires expert verification.The paper motivates intermediate human oversight and reproducible checks rather than unreviewed end-to-end conclusions.Source: §1 · pp. 1–2
  • Human experts retain control of scope and verification while LLMs propose proofs, counterexamples, and auxiliary claims that are refined into checkable results.The workflow records model interactions, rejected routes, and validated statements.Source: §1 · pp. 2–3

1. Topic conceptualization with AI.

  • AI-assisted research spans topic conceptualization, fixed-target theorem proving, and open-ended theorem discovery, with experts selecting and formalizing the useful outputs.The paper also presents prompt records and reusable workflow materials.Source: §1 · p. 3, §2 · p. 3, §3 · p. 3

4. Documented case studies in mathematical optimization.

  • The case studies document Grover-compatible optimization results and distinguish reproduced or adapted mathematics from results introduced in this workflow exposition.The paper states that generalizability beyond its documented case studies remains untested.Source: §4 · pp. 3–4

2. Preliminaries for mathematical research.

  • The paper frames mathematical research as five connected phases: topic conceptualization, conjecturing, validation, proof development, and writing.Conjecture selection still depends on expert judgment.Source: §2 · pp. 4–5

1. Fix bug.

  • Common conjecturing routes include repairing existing methods, weakening assumptions, and combining complementary mechanisms.Examples include robustness to nonsmooth terms, guarantees under perturbations, and combining acceleration with variance reduction.Source: §1 · p. 5, §2 · p. 5, §3 · p. 5

4. Cross domain lifts.

The workflow uses cross-domain reframing, unifying viewpoints, and boundary tests to turn broad research directions into precise, checkable questions. In the Grover and Riemannian-optimization example, AI sketches candidate connections and proof routes, while humans refine assumptions and plan validation.

4. Cross domain lifts.

  • Cross-domain lifts recast a problem in another domain, such as moving from discrete to continuous settings or from Euclidean spaces to manifolds.The paper gives continuous-time ODE and Lyapunov analysis as an example outside its case study.Source: §4 · p. 5

5. Unifying viewpoints.

  • A unifying viewpoint places related methods in one framework to explain their similarities and differences.A parameterized ODE and Lyapunov framework can organize analyses of different acceleration schemes.Source: §5 · p. 5

6. Boundary and negative results.

  • Candidate claims are tested on examples and boundary cases, with feedback used to revise assumptions and decide which directions merit proof.Experts may use calculations and small numerical experiments as diagnostic evidence, while retaining responsibility for assessing the checks.Source: §6 · pp. 5–6

3.1. Early stage exploration with domain sketches and candidate ques-

  • Early exploration uses domain sketches to map mathematical objects, assumptions, objectives, and analogies before proposing research questions.Proposals are paired with claim sketches, nearby classical results, feasibility checks, and novelty and tractability judgments.Source: §3.1 · pp. 6–7

3.2. Concrete idea phase for sharpened claims and validation planning.

  • The concrete-idea phase fixes notation and assumptions, organizes proof tasks, and plans tests before shaping the paper’s structure.For the Grover example, AI suggests relevant objects, candidate submanifolds, and gradient-to-iteration correspondences for human refinement.Source: §3.2 · p. 7

4. AI-assisted theorem proving.

The paper describes fixed-target proving as a process in which humans set goals and verify AI-generated arguments, while uncertain claims receive coordinated proof and disproof searches. In the richer Grover-related example, a model-suggested subspace observation is developed into a human-formulated low-dimensional scalar update result.

4. AI-assisted theorem proving.

  • Prompt records document the provenance of model suggestions, while the manuscript records human selection, formalization, verification, and integration.The case-study results include material originating in or adapted from the companion mathematical article [20].Source: §4 · p. 8, §4.2 · p. 10

4.1. Direct proofs when the statements are trusted.

  • For trusted statements, the model drafts stepwise proofs and local variants, but experts check assumptions, calculations, edge cases, and cited results before integrating a rigorous argument.The illustrated theorem states that vanishing Riemannian gradient is equivalent to global optimality, with objective value 0 or 1.Source: §4.1 · pp. 8–9

4.2. Clear target, uncertain truth.

  • For uncertain claims, coordinated proof and disproof branches search for arguments and counterexamples so that humans can assess the evidence without one-sided reasoning.The commutator example concerns whether commutators of Hermitian matrices equal the traceless skew-Hermitian matrices su(n).Source: §4.2 · pp. 9–10

4.3. Rich proofs and the “Aha” moment.

  • A model-generated observation about confinement to the Grover plane was refined by human authors into a scalar process tracking the high-dimensional dynamics.For the specified product and parameter rule, the update is a three-dimensional real process that preserves the Grover plane and admits closed-form scalar recursions.Source: §4.3 · p. 10

5. AI-assisted theorem discovery.

This section describes a human-guided AI workflow for proposing evidence-backed candidates, proof routes, and parameter choices, which experts test and refine into verified theorems and reusable structure. It also presents a refinement that uses the objective’s geometry to replace a smoothness-based guarantee with a PL-based convergence result checked by human experts.

5.1.1. AI-guided proposal of candidate conclusions.

  • The exponential update preserves the Grover plane, yields a scalar recursion, and admits a one-shot optimum for 0 < q0 < 1; at q0 = 0 or 1 finite steps leave the state unchanged.The q0 = 0 endpoint cannot reach f = 1, while q0 = 1 is already optimal.Source: §5.1.1 · pp. 11–12

5.1.2. Human abstraction and cross-setting transfer.

  • Theorem 5.1 establishes that products generated by H and ψ0 preserve a fixed two-dimensional Grover subspace and keep the tangent gradient in a fixed two-direction span.The resulting invariant and closure statements form a portable schema; related settings such as VQE, QAOA-style ansatzes, and amplitude-amplification variants are proposed for future validation.Source: §5.1.2 · pp. 12–13

5.2. Property constrained synthesis.

  • The property-constrained search selects a length-5 product retraction as the shortest candidate passing screening, with its specified product form and initial velocity then verified symbolically.The search checks that factors are generated by H and ψ0, that V(0; x, y) = I, and that the initial velocity equals Z.Source: §5.2 · pp. 13–14

5.3.1. Scoping with AI for objects, ambient spaces, and assumptions.

  • AI-assisted scoping fixes the theorem’s domain as U(N) with its canonical Riemannian metric, specifies the objective and Lipschitz-gradient assumption, and defines the target iteration-bound problem.Human experts review and revise the checklist of objects, assumptions, boundary cases, and notation until the statement is internally consistent.Source: §5.3.1 · p. 15

5.3.2. Route confirmation through a literature guided plan.

  • The literature-guided route rejects a Euclidean Lipschitz analysis as mismatched to the target rate and adopts a Riemannian gradient-descent result based on for the retraction method.With fixed step size t = 1/LRie, the stated iteration achieves the targeted convergence rate; the proof plan then requires bounding LRie and checking the theorem’s assumptions.Source: §5.3.2 · pp. 15–16

5.3.3. Parameter discovery:

  • The parameter-discovery loop proposes and tests constants, then establishes globally tight first- and second-order retraction bounds, with ratios tending to 1 and 1/(4c0), respectively.The candidate values α = 1 and β = 1/(4c0) are adopted after symbolic verification; numerical stress tests help identify candidates but the theorem relies on proof and tightness arguments.Source: §5.3.3 · p. 17

5.3.4. Refining the theorem through structural insights and improved results.

  • The refinement stage uses verified structural conditions such as a Polyak-Łojasiewicz inequality to strengthen convergence analysis without changing the underlying algorithm.The aim is to improve rates, weaken assumptions, or simplify constants in the baseline theorem.Source: §5.3.4 · p. 17
  • The baseline O(ε^-2) guarantee applies to general nonconvex smooth functions; structural analysis of the specific objective identifies a local PL inequality for refinement.The model suggests the PL route, and human experts check the verification steps and proof.Source: §5.3.4 · pp. 17–18
  • The refined guarantee requires the initial iterate to lie in the region where the pullback-gradient smoothness bound and PL inequality hold, with all subsequent iterates remaining there.The theorem does not establish entry into this region from an arbitrary initialization.Source: §5.3.4 · p. 18
  • Theorem 5.5 guarantees an optimality gap of at most ε within a finite iteration bound under its stated PL and smoothness assumptions.The supplied theorem passage truncates the expression for the iteration bound, so no rate is reported here.Source: §5.3.4 · p. 18, Table 3 · p. 18

6. Roles of human and AI.

Human authors define the mathematical specification and filter model proposals through case-specific checks; prompt and failure records document that division of labor. The workflow depends on expert verification and treats proof assistants as complementary.

6. Roles of human and AI.

  • Human authors fix the objects, assumptions, admissible operations, and acceptance criteria; the LLM proposes proof routes, lemmas, counterexamples, constructions, and checks within that frame.In the Grover case study, authors use the Grover plane, projector identities, scalar recursions, endpoint regimes, and small matrix tests to repair or reject proposals.Source: §6 · p. 18
  • Prompt and failure records show model suggestions, the checks applied, and which proposals were accepted, repaired, or rejected.Multi-oracle examples include an intersection oracle outside the gate model, updates that lost the average-gradient structure, and matrix-product convention errors.Source: §6 · p. 19
  • The workflow presupposes domain experts who can detect shifted assumptions, notation drift, missing arguments, and misuse of standard lemmas.It is primarily a natural-language proof workflow, with prompt records, Python checks, and partial auxiliary formalization; proof assistants can provide stronger certification after statements stabilize.Source: §6 · p. 19

7. Conclusion.

The conclusion presents a human-in-the-loop workflow in which experts set scope, check model suggestions, and choose which statements enter the paper. In the case study, the refinement reaches a PL-based complexity bound under stated regional assumptions, and the records document how proposals were handled.

7. Conclusion.

  • Human experts set the mathematical scope, check model suggestions, and decide which statements enter the paper.The LLM explores possible proofs, counterexamples, and auxiliary claims inside that frame.Source: §7 · p. 19
  • The case study refines a generic smooth guarantee to a PL-based complexity bound, assuming iterates already lie in and remain where the PL inequality and pullback-gradient smoothness bound hold.The conclusion describes the workflow as exploring proofs, counterexamples, and auxiliary claims within a human-defined frame.Source: §7 · p. 19
  • The reporting format records model proposals, verification, rejected or corrected routes, and validated statements incorporated into the paper.The case study produces checkable records while organizing refinement of the convergence guarantee.Source: §7 · p. 19

Declarations

The authors declare no relevant financial interests.

Declarations

Appendix A. Grover-related supplementary case study and prompt records.

The appendix provides prompt records and reusable templates, computational details, and a related multi-oracle exploration. That exploration combines pattern-based reductions and numerical diagnostics with checks for transfer-specific assumptions and representative failure routes.

Appendix A. Grover-related supplementary case study and prompt records.

  • The appendix provides shortened prompt–response materials, reusable templates, finite-difference retraction checks, and auxiliary formalization code in a public repository.Templates include slots for assumptions, admissible operations, boundary cases, and verification checks.Source: Appendix A · pp. 19–20
  • Main-case interactions used GPT-5.1 via web chat from September through December 2025; numerical checks were small CPU-based matrix tests on an Apple M4 MacBook Pro.The machine had a 10-core CPU and 24 GB memory, and the checks used Python 3.10.Source: Appendix A · p. 20

A.1. Multi-oracle case study.

  • The multi-oracle case study replaces one oracle projector with several and examines which workflow components transfer and which require new checks.It is related to, but outside, the main theorem sequence.Source: §A.1 · p. 20
  • For commuting projectors, joint membership patterns reduce the relevant state components to a span of nonzero E_b|ψ0⟩ vectors of dimension at most 2^r.In this basis, the averaged objective and average-gradient direction become finite-dimensional objects comparable with full matrix simulations.Source: §A.1 · p. 20
  • In the fully active two-oracle representation, the constructed matrices form a real basis for the average-gradient subspace.The frame check tests whether Bavg columns lie in the real column span of Bdet, using five deterministic and 200 random positive pattern-weight configurations.Source: §A.1 · p. 21
  • The tested two-oracle construction had a largest least-squares projection residual of 2.029 × 10^-13 and a maximum state-vector discrepancy of 2.091 × 10^-15 between reduced and full simulations.For N from 64 through 16384, the log–log regression of iteration counts on N had slope 0.542181.Source: §A.1 · p. 21
  • Multi-oracle transfer requires additional checks for gate-model admissibility, consistency with the average Riemannian gradient, and matrix-product order; several natural routes instead solved another problem or lost required structure.The recorded failures also include implicit implementation-convention errors.Source: §A.1 · p. 21

A.2. Representative failed routes from the second multi-oracle case study.

The multi-oracle case study records four representative failure modes and how human checks corrected or rejected proposed routes. It also indexes prompts for the main Grover-compatible case study.

A.2. Representative failed routes from the second multi-oracle case study.

  • Four selected failures include an inadmissible intersection oracle, an incompatible direction, a matrix-product convention error, and overstrong numerical convergence language.The cases are illustrative, not an exhaustive or randomly sampled set, and support no inference about general response frequency or performance.Source: §A.2 · pp. 21–22
  • The intended gate model allows phase gates generated by ψ0 and the individual Hj projectors, so an intersection phase gate changes the model.The model-generated intersection-oracle route was rejected, and the prompt was tightened to require updates built from the admissible gates.Source: §A.2 · pp. 21–22
  • A component direction may increase one score yet fail to follow the average-gradient direction, which depends on the sum of all component commutators.Related projected-gradient variants stalled away from the intersection when projection removed components needed for progress.Source: §A.2 · p. 22
  • A valid multi-oracle update must use admissible gates and remain compatible with the Riemannian gradient of the stated objective.The later frame-compatible route preserved the original gate model, but its frame condition required the standard convention that the rightmost matrix factor acts first.Source: §A.2 · p. 22
  • Numerical tests suggested average objective values approaching 1, while the analysis established stationarity under the stated assumptions.The authors therefore weakened the convergence wording rather than treating the experiments as proof of objective convergence.Source: §A.2 · p. 22
  • Human correction also replaced an initially random frame construction with an explicit deterministic frame and direct span check.A mathematically relevant dynamical-Lie-algebra framing was removed from the algorithmic main line as poorly aligned with the intended optimization presentation.Source: §A.2 · p. 22
  • Table 4 summarizes the four selected failure modes by symptom, check, and disposition.These examples are not exhaustive or randomly sampled and do not establish a base rate for correct, salvageable, or unusable outputs.Source: §A.2 · p. 22, Table 4 · p. 23

A.3. Prompt records for the main Grover-compatible case study.

  • The remaining appendix entries index prompt families used in the main Grover-compatible case study.The prompt index covers scoping, route framing, proof, discovery, transfer, retraction synthesis, theorem specification, and rate refinement.Source: §A.2 · p. 23, Appendix label · p. 23

A.3.1. Prompts for Section 3.1.

The prompt records turn broad research ideas into checkable mathematical tasks, with experts reviewing model suggestions before incorporating them. The Grover example illustrates how a model-suggested invariant subspace was developed into a result supporting scalar tracking.

A.3.1. Prompts for Section 3.1.

  • The scoping prompt asks for relevant quantum and optimization objects, candidate research directions, assumptions, nearby results, and feasibility notes.It requests concrete, numbered directions rather than disconnected speculation.Source: §A.3.1 · p. 24

A.3.2. Prompts for Section 3.2.

  • The Grover-framing prompt asks for precise objects on both sides, including a quantum-state manifold and Riemannian gradient updates, then requests symmetry and complexity alignment checks.It also asks which regimes or limits make the discrete Grover iterations structurally coincide with gradient-like updates.Source: §A.3.2 · p. 24

A.3.3. Prompts for Section 4.1.

  • The direct-proof prompt requires assumptions and domains to be restated and every nontrivial inference justified line by line.It asks for adversarial checks and forbids fabricated references; humans retain responsibility for verifying citation support.Source: §A.3.3 · pp. 24–25
  • The fixed-target proof prompt requests both directions of the claim linking a zero gradient to global optimality, including objective values in {0, 1}.The requested proof specifically explains why grad f(U) = 0 is equivalent to [H, ψU] = 0.Source: §A.3.3 · p. 25

A.3.4. Prompts for Section 4.2.

  • The prove-or-disprove prompt runs proof and counterexample searches in parallel before requiring a final verdict with a proof or explicit counterexample.It calls for stated assumptions, line-by-line reasoning, standard facts, and human adversarial checks.Source: §A.3.4 · p. 25

A.3.5. Model reply for Section 4.3.

  • The model reply identifies an invariant two-dimensional Jordan plane K = span{|ψ0⟩, H|ψ0⟩} for the projector-driven evolution.On this subspace the operators act as 2 × 2 matrices, with overlap angle θ0 = arccos √q0.Source: §A.3.5 · pp. 25–26
  • The authors developed the subspace observation into a theorem that replaces high-dimensional operations with classically trackable scalar recurrences in (xk, yk, qk).The observation is described as reducing the dynamics to SU(2) rotations.Source: §A.3.5 · p. 26

A.3.6. Prompts for Section 5.1.1.

The prompt templates specify fixed settings while leaving conclusions open, then direct the model to propose and test candidate statements or constructions. Human review and proof remain part of selecting and finalizing the results.

A.3.6. Prompts for Section 5.1.1.

  • The discovery prompt fixes the assumptions and notation for a projector-driven update while leaving its conclusions open.It asks for candidate invariants, identities, dimensional reductions, stability properties, and convergence statements.Source: §A.3.6 · p. 26
  • The model is asked to restate assumptions, propose typed candidate claims, and combine tested survivors into a proposition with justified derivations.The template requests lightweight pass/fail/inconclusive tests and adversarial checks.Source: §A.3.6 · pp. 26–27

A.3.7. Prompts for Section 5.1.2.

  • The cross-setting transfer prompt seeks a reusable schema built from an invariant subspace, gradient or tangent plane, scalar progress coordinate, and structured update.It then asks for analogues and proofs in a product setting.Source: §A.3.7 · p. 27

A.3.8. Prompts for Section 5.2.

  • The retraction-synthesis prompt fixes admissible projector gates and tangent targets, then requests candidate gate products satisfying specified properties.Candidates are compared by product length and parameter coupling, with executable finite-difference tests and symbolic viability checks.Source: §A.3.8 · pp. 27–28
  • The selected retraction candidate must be stated with final parameter constraints and a proof plan for the target properties.The prompt also asks for executable tests and adversarial checks; the template harmonizes its curve notation with Theorem 5.2.Source: §A.3.8 · pp. 27–28

A.3.9. Prompts for Section 5.3.1.

  • The theorem-specification prompt asks the model to define the ambient space, metric, gradient, assumptions, and feasible proof routes for a rough target.It also requests relevant literature and warnings about standard results or counterexamples.Source: §A.3.9 · p. 28

A.3.10. Prompts for Section 5.3.2.

The prompts examine Riemannian complexity and retraction bounds, then ask whether the Grover objective’s structure sharpens a baseline rate. A separate composite-optimization case develops an effective curvature scale and a two-sided route to bounds.

A.3.10. Prompts for Section 5.3.2.

  • The Riemannian-complexity prompt contrasts ambient Euclidean smoothness with Lipschitz control of the Riemannian or pullback gradient.It asks for references and a generic retraction-based complexity theorem with its structural assumptions.Source: §A.3.10 · pp. 28–29

A.3.11. Prompts for Section 5.3.3.

  • The retraction prompt defines a length-5 product retraction on U(N) and requests global constants bounding first- and second-order approximation errors.It asks for numerical tests before theoretical justification and a comment on tightness.Source: §A.3.11 · p. 29

A.3.12. Prompts for Section 5.3.4.

  • The Grover convergence prompt treats the established generic smooth non-convex rate O(ε^-2) as a baseline and asks whether the trace objective’s structure yields a faster rate.It specifically asks for a gradient-norm versus function-gap relation and a refined iteration bound.Source: §A.3.12 · pp. 29–30

Appendix B. Separate case study: composite (L0, L1)-smooth convex optimization.

  • The composite case studies min F(x) = f(x) + h(x) under gradient-dependent smoothness and poses upper-bound, lower-bound, and oracle-access questions.Its scope includes a nonempty solution set, a bounded initial distance, and a subgradient bound G⋆ at an optimum.Source: Appendix B · p. 30

B.1. Problem scoping.

  • The proposed effective curvature scale is L⋆ = L0 + L1G⋆ because the composite optimum may have ∇f(x⋆) = −v⋆ rather than zero.The authors retain this scale and a two-sided upper- and lower-bound roadmap, with lower-order logarithmic terms allowed.Source: §B.1 · pp. 30–31

B.2. Structural discovery.

  • Affine recentering makes ∇ϕ(x⋆) = 0 while the unknown v⋆ cancels from the complete proximal-gradient step.The finalized centered gradient–gap relation supplies adaptive curvature control for the subsequent analysis.Source: §B.2 · p. 31

Appendix B. Separate case study: composite (L0, L1)-smooth convex optimization.

  • The composite case retains adaptive step sizes tied to the centered gradient and a Lyapunov recursion, with an explicit rule and two-phase analysis replacing tentative localization.The case-study account says authors complete and verify the final statements and proofs after model contributions to the research route and mechanisms.Source: Appendix B · p. 30, §B.2 · p. 32

B.3. Upper-bound development and human proof reconstruction.

The upper-bound route combines an auxiliary-sequence potential with a two-phase analysis, while the lower-bound route uses an orthogonal-coordinate embedding to preserve the hard instance against proximal queries.

B.3. Upper-bound development and human proof reconstruction.

  • Under the warm-start condition, the potential contracts by 1 + αk and is bounded by ΓkR2, yielding geometric large-error reduction and an accelerated small-error phase.The displayed scheme assumes valid R and G⋆ bounds; without them, a doubling or backtracking wrapper is required.Source: §B.3 · p. 32

B.4. Lower-bound discovery and correction.

  • The lower-bound construction uses orthogonal coordinates so the proximal map reveals no additional information about the hard block, transferring the classical smooth lower bound [5].The claim is restricted to span-respecting deterministic proximal first-order methods whose final output is a queried point.Source: §B.4 · p. 32, §B.3 · p. 32
  • The finalized record presents one combined summary theorem, with the complete algorithm, five supporting lemmas, two proofs, and exact constants in the companion materials.The same-space affine tilt was rejected because the hard gradient could cancel the added G⋆ component away from the optimum.Source: §B.3 · p. 32, §B.4 · p. 33

B.5. Final conclusion and detailed proof record.

The theorem gives an adaptive accelerated proximal-gradient upper bound for composite (L0, L1)-smooth convex objectives and a matching leading-order lower bound in a restricted oracle model. Its tight leading dependence is L⋆/ε, with lower-order logarithmic terms retained in the upper bound.

B.5. Final conclusion and detailed proof record.

  • The theorem concerns F = f + h with convex, twice-differentiable f satisfying the stated generalized-smoothness condition and proper, closed, convex, proximable h.It also assumes an optimizer x⋆ and a subgradient certificate v⋆ at x⋆, with G⋆ ≥ 0.Source: §B.5 · p. 33
  • Under the theorem's assumptions, the adaptive accelerated proximal-gradient method reaches F(yN) − F⋆ ≤ ε in the stated iteration bound.The supplied theorem passages do not expose the complete bound expression.Source: §B.5 · p. 33
  • L⋆/ε is the tight leading-order dependence in the stated oracle model, while the upper bound retains lower-order logarithmic terms.The lower-bound claim concerns span-respecting deterministic proximal first-order methods whose final output is one of their queried points.Source: §B.5 · p. 33

Related papers

Loading 2512.09443v3…