Operations research, mathematical programming
The Lean Pool projects whose card's first MSC2020 code is in class 90, “Operations research, mathematical programming”: 6 articles, one per card.
TheoremCounterexample to Goemans' unsplittable-flow cost conjecture#
Refutes Goemans' cost conjecture for single-source unsplittable flow, Conjecture 1.3 of Traub, Vargas Koch, and Zenklusen's paper. A simple, loopless, acyclic graph with seven vertices and nine arcs admits a splittable flow of cost 58, but every unsplittable routing within the additive maximum-demand capacity bound costs at least 60, attained by an explicit routing. The development proves completeness of the walk enumeration and transfers the refutation from integers to any linearly ordered commutative ring, including the rationals and reals. Jason Hickey directed Claude's formal verification of the counterexample discovered by Dmitry Rybin with GPT-5.6 Pro; upstream also acknowledges Katherine Schlitz. Planarity is not part of the formalized claim.
Quoted from the card LeanPool/projects/goemans-cost-counterexample.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
GoemansFlow.goemans_cost_conjecture_false(theorem; a main declaration), declared in LeanPool/GoemansFlow/Counterexample.lean, line 577: “The rational form of Goemans' cost conjecture is false, even for simple, loopless, acyclic finite digraphs with explicit capacities, positive demands, and distinct terminals different from the source.” Its source, as the card gives it: “Conjecture 1.3 of arXiv:2308.02651v1”GoemansFlow.not_GoemansCostConjectureFull(theorem), declared in LeanPool/GoemansFlow/Counterexample.lean, line 562: “The same cost conjecture is false over every linearly ordered commutative ring, by transfer of the integer counterexample.”GoemansFlow.optimum_is_sixty(theorem), declared in LeanPool/GoemansFlow/Counterexample.lean, line 405: “On the explicit seven-vertex, nine-arc instance, the minimum cost among unsplittable routings satisfying the additive maximum-demand capacity bound is exactly 60.”GoemansFlow.fractional_cost(theorem), declared in LeanPool/GoemansFlow/Counterexample.lean, line 129: “The given splittable flow on the counterexample instance costs exactly 58.”GoemansFlow.path_complete(theorem), declared in LeanPool/GoemansFlow/Counterexample.lean, line 255: “For each of the three terminals, the lists of arcs giving a walk from the source are exactly the two explicitly exhibited paths.”
Project
- Authors: Jason Hickey.
- Source: A verified counterexample to Goemans' cost conjecture by Jason Hickey, arXiv:2308.02651.
- Project repository: jyh/dinitz-verify, at commit ffba3523.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 90C35, 05C21.
- In Lean Pool: LeanPool/GoemansFlow, from the card LeanPool/projects/goemans-cost-counterexample.yaml.
Sources
TheoremDuality theory in linear optimization and its extensions#
Formalizes Farkas-like theorems and strong LP duality, including extensions to a linearly ordered field with bot and top.
Quoted from the card LeanPool/projects/duality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
equalityFarkas(theorem), declared in LeanPool/Duality/FarkasBasic.lean, line 43: “Farkas' lemma for linear equalities over nonnegative variables.”inequalityFarkas(theorem), declared in LeanPool/Duality/FarkasBasic.lean, line 128: “Farkas' lemma for linear inequalities over nonnegative variables.”extendedFarkas(theorem; a main declaration), declared in LeanPool/Duality/FarkasSpecial.lean, line 572: “Extended Farkas theorem for matrices and vectors over a linearly ordered field with bot and top.”ValidELP.strongDuality(theorem), declared in LeanPool/Duality/LinearProgramming.lean, line 1151: “Strong duality theorem for extended linear programs.”StandardLP.strongDuality(theorem; a main declaration), declared in LeanPool/Duality/LinearProgrammingB.lean, line 242: “Strong duality theorem for linear programs in standard form.”
Project
- Authors: Martin Dvorak.
- Source: doi:10.46298/afm.14253, arXiv:2409.08119.
- Project repository: madvorak/duality.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 90C05, 90C46.
- In Lean Pool: LeanPool/Duality, from the card LeanPool/projects/duality.yaml.
Sources
TheoremGradient-only acceleration for generalized-smooth convex optimization#
A damped accelerated method minimizes convex functions on real Hilbert spaces whose differentiable gradients satisfy the Hessian-growth bound norm(D gradient f x) <= L0 + L1 * norm(gradient f x). The development proves an explicit gradient-query budget for any positive accuracy, initial distance bound and initial objective-gap bound, with an attained minimum. It retains the oracle execution model, ordinary gradient descent, energy dissipation, charging arguments and two complementary convergence bounds. No objective value or line-search oracle is assumed.
Quoted from the card LeanPool/projects/longtails-generalized-convex.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized.result(theorem; a main declaration), declared in LeanPool/LongTails/Theorems/GeneralizedSelfNormalizedConvex.lean, line 32: “For positive L0, R, Delta and epsilon and nonnegative L1, a single damped accelerated algorithm returns a point of objective gap at most epsilon for every admissible convex objective with an attained minimum within distance R and initial objective gap at most Delta. Its exact gradient-query budget is zero when Delta <= epsilon; otherwise it is twice the natural ceiling of 4096 times (1 + sqrt(L0*R^2/epsilon) + min(ceil((L1*R)^(2/3))*D, D + (L1*R*D)^(2/3))), where D = log(4 + 4*Delta/epsilon).”LongTails.OracleTemplate.GeneralizedAccelerated.run_accuracy_self_normalized(lemma), declared in LeanPool/LongTails/Proofs/GeneralizedSelfNormalizedConvergence.lean, line 78: “Under the same convexity, gradient, Hessian-growth and initialization hypotheses, N accelerated steps reach objective gap epsilon whenever N >= 4096*(1 + sqrt(L0*R^2/epsilon) + D + (L1*R*D)^(2/3)).”LongTails.OracleTemplate.GeneralizedAccelerated.execute_gradient_oracle(lemma), declared in LeanPool/LongTails/Proofs/DampedGeneralizedExecution.lean, line 59: “Execution with any admissible exact-gradient oracle and a budget of 2*N gradient queries equals the N-step accelerated iterate, for every seed.”LongTails.OracleTemplate.Gradient.gd_accuracy(lemma), declared in LeanPool/LongTails/Proofs/GdConvex.lean, line 135: “For L > 0, R >= 0 and epsilon > 0, a convex function with an exact L-Lipschitz gradient and initial distance at most R from a comparison point, ordinary gradient descent reaches objective gap epsilon after max(1, ceil(L*R^2/(2*epsilon))) queries.”
Project
- Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets.
- Project repository: k3nfalt/longtails, at commit 269cbc76.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 90C25, 90C30, 68Q25.
- In Lean Pool: LeanPool/LongTails, from the card LeanPool/projects/longtails-generalized-convex.yaml.
Sources
TheoremHomogeneous self-dual interior-point method for linear programming#
Formalizes a homogeneous self-dual interior-point method for linear programming, including primal-dual data, Newton block solvability from full row rank, fixed Ye-Todd-Mizuno predictor/corrector local estimates, contraction bounds, and logarithmic stopping certificates for generated iterates.
Quoted from the card LeanPool/projects/hsd-interior-point-lp.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
HSDInteriorPointLP.YTM_fixed_local_theory_from_paper(theorem; a main declaration), declared in LeanPool/HSDInteriorPointLP/FixedYTMTheory.lean, line 1007: “Packages the fixed Ye-Todd-Mizuno local theory, combining predictor and corrector estimates for the tight and wide central neighborhoods.” Its source, as the card gives it: “Y. Ye, M. J. Todd, and S. Mizuno, An O(√nL)-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1):53-67, 1994.”HSDInteriorPointLP.HSDGeneratedAlgorithm.gap_stop_even_at_logPairBound(theorem), declared in LeanPool/HSDInteriorPointLP/GeneratedConvergence.lean, line 253: “Proves that the generated even iterate satisfies the gap stopping test at the logarithmic pair bound.”HSDInteriorPointLP.HSDGeneratedAlgorithm.mu_stop_even_at_logPairBound(theorem), declared in LeanPool/HSDInteriorPointLP/GeneratedConvergence.lean, line 279: “Proves that the generated even iterate satisfies the duality-measure stopping test at the scaled logarithmic pair bound.”HSDInteriorPointLP.HLP_newton_block_system_solvable_from_full_row_rank(theorem), declared in LeanPool/HSDInteriorPointLP/NewtonSystem.lean, line 808: “Shows solvability of the Newton block system from the full-row-rank assumption through finite-dimensional linear algebra.”HSDInteriorPointLP.YTM_contraction_power_le_exp(theorem), declared in LeanPool/HSDInteriorPointLP/FixedYTMTheory.lean, line 1170: “Bounds the fixed YTM contraction power by the corresponding exponential decay estimate.”
Project
- Authors: Makoto Yamashita.
- Source: An O(√nL)-iteration homogeneous and self-dual linear programming algorithm by Yinyu Ye, Michael J. Todd, Shinji Mizuno, doi:10.1287/moor.19.1.53.
- Project repository: makoto-yamashita/proof-on-a-homogeneous-self-dual-interior-point-method-for-linear-programming.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 90C05, 90C51.
- In Lean Pool: LeanPool/HSDInteriorPointLP, from the card LeanPool/projects/hsd-interior-point-lp.yaml.
Sources
TheoremParameter-Free Gradient Minimization in l_p Geometry#
Exact value-gradient query-complexity results for convex differentiable objectives on finite-dimensional real l_p spaces with attained minima and a positive global primal-to-dual Lipschitz-gradient bound. For finite real p > 1, the development proves strict-local scale-identification impossibility at LR/epsilon = 4 and a deterministic method family with three post-secant-initialization query-rate regimes. For p > 2 it also proves deterministic known-parameter upper and lower query exponents p/(p+2), with explicit horizon and dimension restrictions on the lower bound.
Quoted from the card LeanPool/projects/parameter_free_gradient_p.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
V7.scaleIdentificationImpossibility(theorem), declared in LeanPool/ParameterFreeGradient/V7/Proofs/Stage7StrictRandomizedExpected/Closure.lean, line 21: “For finite real p > 1 and positive epsilon, measurable strict-local exact value-gradient methods satisfy scale-identification lower bounds on convex smooth one-dimensional objectives with unique minimizers, even at LR/epsilon = 4. The result includes deterministic and randomized finite-horizon statements and infinite worst-case expected queried-or-returned hitting time.”V7.knownParameterAboveTwoOptimality(theorem), declared in LeanPool/ParameterFreeGradient/V7/Proofs/Stage5AboveTwoLowerS5F/Optimality.lean, line 19: “For finite real p > 2 and convex differentiable objectives with attained minima and a positive global primal-to-dual Lipschitz-gradient bound, deterministic known-parameter exact value-gradient methods have upper query exponent p/(p+2). The matching lower exponent concerns the first T queries, requires d >= 2 and 1 <= T <= d, and retains the explicit min(p, log d) dependence.”V7.main(theorem; a main declaration), declared in LeanPool/ParameterFreeGradient/V7/Proofs/Stage8Main/Main.lean, line 186: “For convex differentiable objectives with attained minima and positive global L-Lipschitz gradients from l_p to its dual, one deterministic family works for every finite real p > 1 and positive epsilon after supplied nondegenerate secant initialization with 0 < M0 <= L. It returns a queried point with dual gradient norm at most epsilon. Writing R for distance to the minimizer set, the post-initialization oracle-call bound has polynomial dependence on max(1, LR/epsilon) with exponent 1/2 for 1 < p < 2 and p = 2, and p/(p+2) for p > 2, plus additive log(e + L/M0) calibration cost. Constants depend only on p, with a universal constant at p = 2; discovering the secant pair is outside the count.”
Project
- Authors: Yuning Yang.
- Project repository: yuningyang19/parameter_free_gradient_p, at commit f71215fa.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 90C25.
- In Lean Pool: LeanPool/ParameterFreeGradient, from the card LeanPool/projects/parameter_free_gradient_p.yaml.
Sources
TheoremPersistent failure of quartic sum-of-squares exactness#
Constructs explicit rational cubics in fourteen real variables whose Euclidean quartic regularizations have a strict ordinary sum-of-squares gap for every positive regularization, quadratic, and cubic parameter. A companion construction has a unique global minimizer and a positive-definite Hessian there. Exact moment certificates and a general SOS degree bridge certify the gap for arbitrary finite sums of squares of real polynomials.
Quoted from the card LeanPool/projects/persistent-sos.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PersistentSOS.persistent_failure(theorem; a main declaration), declared in LeanPool/PersistentSOS/Main.lean, line 88: “For every positive sigma, a, and b, the explicit fourteen-variable quartic sigma/4 times the Euclidean norm to the fourth power minus a/2 times the squared norm minus b times the displayed cubic has the stated attained global minimum, and subtracting that minimum is not an ordinary finite sum of squares of real polynomials.”PersistentSOS.unique_persistent_failure(theorem; a main declaration), declared in LeanPool/PersistentSOS/UniqueMain.lean, line 60: “For all three positive parameters, the companion quartic has exactly one global minimizer, its actual polynomial Hessian is positive definite there, and its shift by the attained minimum is not an ordinary sum of squares.”PersistentSOS.quantitative_sos_gap(theorem), declared in LeanPool/PersistentSOS/Main.lean, line 54: “For positive sigma and a and any real b, every ordinary sum-of-squares lower bound is at most the stated minimum-value expression minus b times 753357629/500000000000 times the cube of the stated radius. When b is positive, that expression is the attained global minimum.”PersistentSOS.sphere_moment_gap(theorem), declared in LeanPool/PersistentSOS/Main.lean, line 97: “An explicit linear functional on real polynomials has normalized radial moments, is nonnegative on all quadratic squares, annihilates the quadratic sphere localizers, and evaluates the cubic to 500753357629/500000000000, strictly above its sphere maximum of one.”
Project
- Authors: JD Jones.
- Source: Persistent SOS failure with an explicit unique global minimizer by JD Jones.
- Project repository: JD-Jones-ASES/persistent-sos, at commit d432ff9a.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 90C22, 90C26, 14P10.
- In Lean Pool: LeanPool/PersistentSOS, from the card LeanPool/projects/persistent-sos.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.