A note on the parameter ell in Buchbinder--Feldman's deterministic submodular matroid algorithm
Pith reviewed 2026-05-07 10:18 UTC · model grok-4.3
The pith
Tighter bounds on (1+1/ℓ)^{-ℓ} allow a reduced parameter ℓ of order 1/(2eε) in Buchbinder-Feldman's deterministic algorithm, improving the query complexity constant.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The note establishes that the Pólya–Szegő inequality (1+1/ℓ)^{-ℓ} ≤ e^{-1}(1+1/(2ℓ)) can be used in place of a looser estimate in the proof of Buchbinder and Feldman, thereby allowing the choice ℓ = ⌈1/(2eε)⌉ while still ensuring the (1−1/e−ε) approximation. This yields an improvement to the implicit constant in the Õ_ε(nr) query bound by a factor ≈2^{0.816/ε}. In addition, the alternating-series bound (1+1/ℓ)^{-ℓ} ≤ e^{-1} exp(1/(2ℓ)−1/(3ℓ^2)+1/(4ℓ^3)) matches the true asymptotic expansion through ℓ^{-3} and gives ℓ_∗ = 1/(2eε) − 5/12 + O(ε). The asymptotic complexity class remains Õ_ε(nr) in both cases, with only the ε-dependent constant refined, and all steps are machine-checked in Lean 4
What carries the argument
The integer parameter ℓ and the upper bound applied to the expression (1 + 1/ℓ)^{-ℓ} in the error analysis of the deterministic approximation algorithm.
If this is right
- The ε-dependent factor in the query complexity Õ_ε(nr) is reduced by approximately 2^{0.816/ε}.
- The (1-1/e-ε) approximation guarantee continues to hold for the deterministic algorithm.
- The algorithm procedure requires no changes beyond selecting the smaller value of ℓ.
- The sharper bound gives a more accurate asymptotic for the optimal ℓ as ε → 0.
- The Lean 4 formalization verifies the supporting inequalities rigorously.
Where Pith is reading between the lines
- Implementing the algorithm with the reduced ℓ could make it feasible for smaller ε values where the original constant was too large.
- Analogous tightenings using classical inequalities may apply to other analyses in submodular optimization.
- The use of proof assistants like Lean suggests a template for certifying more algorithmic results.
- Further improvements would likely require different bounding techniques since the second bound is asymptotically tight.
Load-bearing premise
The assumption that the original proof structure remains valid after replacing the bound on (1+1/ℓ)^{-ℓ} with these tighter versions, without needing adjustments to the algorithm or loss of the approximation guarantee.
What would settle it
A concrete monotone submodular function and matroid instance on which the algorithm with ℓ = ⌈1/(2eε)⌉ returns a solution whose value is strictly less than (1 - 1/e - ε) times the optimal value.
read the original abstract
Buchbinder and Feldman recently gave a deterministic $(1-1/e-\varepsilon)$-approximation for maximizing a non-negative monotone submodular function subject to a matroid constraint, with query complexity $\widetilde{O}_\varepsilon(nr)$. Their algorithm uses an integer parameter $\ell$, which Buchbinder and Feldman fix to $\ell = 1 + \lceil 1/\varepsilon \rceil$ via a loose bound on $(1+1/\ell)^{-\ell}$. We point out two purely elementary refinements. First, the classical P\'olya--Szeg\H{o} inequality $(1+1/\ell)^{-\ell} \le e^{-1}(1+1/(2\ell))$ replaces the loose step in their proof and permits $\ell = \lceil 1/(2e\varepsilon) \rceil$, shrinking the hidden constant in $\widetilde{O}_\varepsilon(nr)$ by a factor $\approx 2^{0.816/\varepsilon}$. Second, an alternating-series tail bound for $\log(1+t)$ yields the asymptotically sharp inequality $(1+1/\ell)^{-\ell} \le e^{-1}\exp(1/(2\ell) - 1/(3\ell^2) + 1/(4\ell^3))$, matching the true expansion of $(1+1/\ell)^{-\ell}$ through order $\ell^{-3}$ and translating into $\ell_\star = 1/(2e\varepsilon) - 5/12 + O(\varepsilon)$. The asymptotic class $\widetilde{O}_\varepsilon(nr)$ of the query complexity is unchanged in either case; only the implicit constant in $\varepsilon$ is improved. All inequalities in this note are formalized and machine-checked in Lean 4 against Mathlib.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper is a short note identifying a loose bound on (1+1/ℓ)^{-ℓ} in the analysis of Buchbinder and Feldman's deterministic (1-1/e-ε)-approximation algorithm for monotone submodular maximization under a matroid constraint. It replaces the loose step with the classical Pólya–Szegő inequality to obtain ℓ = ⌈1/(2eε)⌉ (improving the hidden constant in the Õ_ε(nr) query complexity by a factor ≈2^{0.816/ε}) and with an alternating-series tail bound on log(1+t) to obtain the asymptotically sharper ℓ_⋆ = 1/(2eε) - 5/12 + O(ε). The note states that the substitution preserves the original approximation guarantee and algorithm, and that all inequalities have been machine-checked in Lean 4 against Mathlib.
Significance. If the direct substitution into the Buchbinder–Feldman analysis is valid, the note supplies a concrete, elementary improvement to the practical dependence on ε in a state-of-the-art deterministic submodular algorithm. The machine-checked Lean 4 formalization against Mathlib is a clear strength, eliminating any doubt about the validity of the new bounds on (1+1/ℓ)^{-ℓ}. The asymptotic query complexity class remains Õ_ε(nr); only the implicit constant is tightened. This is a modest but useful refinement for implementers who care about the precise polynomial dependence on 1/ε.
minor comments (2)
- §1, paragraph after Eq. (1): the phrase 'shrinking the hidden constant in Õ_ε(nr) by a factor ≈2^{0.816/ε}' would benefit from a one-sentence derivation of the exponent 0.816 (i.e., log_2(e)·(1-1/(2e)) or similar) so readers can verify the numerical claim without external calculation.
- The note correctly states that the algorithm and (1-1/e-ε) guarantee carry over unchanged, but a single sentence explicitly confirming that no other place in the original proof uses the looser bound on (1+1/ℓ)^{-ℓ} would remove any residual doubt.
Simulated Author's Rebuttal
We thank the referee for the positive assessment of the note and the recommendation to accept. We are pleased that the elementary character of the refinements and the machine-checked Lean 4 formalization were highlighted as strengths.
Circularity Check
No significant circularity
full rationale
The note improves the parameter ℓ by substituting the external classical Pólya–Szegő inequality and an alternating-series tail bound for log(1+t) into the existing Buchbinder–Feldman analysis. These inequalities are independent facts, machine-checked in Lean 4 against Mathlib, and do not depend on the target approximation guarantee or algorithm. The (1−1/e−ε) guarantee and deterministic procedure carry over unchanged; the only modification is a tighter upper bound on a single term (1+1/ℓ)^{-ℓ}. No derivation step reduces the claimed improvement to a quantity defined in terms of the result itself, no parameters are fitted to data, and the single citation to Buchbinder–Feldman is not load-bearing for the new bound. The argument is therefore self-contained against external benchmarks.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math Pólya–Szegő inequality: (1+1/ℓ)^{-ℓ} ≤ e^{-1}(1 + 1/(2ℓ))
- standard math Alternating-series tail bound for the Taylor expansion of log(1+t)
Reference graph
Works this paper leans on
-
[1]
Niv Buchbinder and Moran Feldman. Deterministic algorithm and faster algorithm for submodular maximization subject to a matroid constraint. To appear inSIAM J. Comput.; preliminary version inFOCS 2024. arXiv:2408.03583v3 (Sept. 2025)
-
[2]
Maximizing a monotone submodular function subject to a matroid constraint.SIAM J
Gruia Călinescu, Chandra Chekuri, Martin Pál, and Jan Vondrák. Maximizing a monotone submodular function subject to a matroid constraint.SIAM J. Computing, 40(6):1740–1766, 2011
work page 2011
-
[3]
George L. Nemhauser and Laurence A. Wolsey. Best algorithms for approximating the maximum of a submodular set function.Mathematics of Operations Research, 3(3):177–188, 1978
work page 1978
-
[4]
Springer, 1972 (English translation); original German edition 1925
George Pólya and Gábor Szegő.Problems and Theorems in Analysis, Volume I. Springer, 1972 (English translation); original German edition 1925. 7
work page 1972
-
[5]
Sanjay K. Khattri. Three proofs of the inequalitye < (1 + 1/n)n+0.5.The American Mathematical Monthly, 117(3):273–277, March 2010.DOI:10.4169/000298910X480126
-
[6]
Sharp inequalities related to the constante.J
Yue Hu and Cristinel Mortici. Sharp inequalities related to the constante.J. Inequal. Appl., 2014:382, 2014
work page 2014
-
[7]
The Lean 4 theorem prover and programming language
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. InCADE-28, pages 625–635, 2021
work page 2021
-
[8]
The Mathlib Community. The Lean Mathematical Library. InCPP 2020, pages 367–381, 2020. 8
work page 2020
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.