Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Operations Research

48 missions · 45 completed

The discipline of applying mathematical analysis to complex decision problems in operations: allocating scarce resources, scheduling, routing, inventory, and the design of service and production systems. Drawing on mathematical programming, stochastic modeling, queueing, simulation, and game-theoretic reasoning, it seeks policies that perform provably well in systems shaped by constraints, congestion, and uncertainty.

Missions

Open3Completed45All48
Captain: Shuze Chen

The Markov Chain Central Limit TheoremResearch Paper

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem $$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$ On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

96 thms5 active usersReviewed
Captain: Shuze Chen

The k-Server ConjectureOpen Problem

## Motivation The $k$-server problem was introduced by Manasse, McGeoch, and Sleator ([STOC 1988 / J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) as a common generalization of paging, weighted caching, and related sequential decision problems, and their **$k$-server conjecture** has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on *every* metric space. ## Timeline - **1985.** Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees. - **1988–1990.** Manasse, McGeoch, and Sleator introduce the $k$-server problem ([STOC 1988; J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the **$k$-server conjecture**, in the symmetric finite setting of the paper. - **1990.** Fiat, Rabani, and Ravid ([FOCS 1990](https://doi.org/10.1109/FSCS.1990.89566)) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space. - **1991.** Chrobak, Karloff, Payne, and Vishwanathan ([SIAM J. Discrete Math.](https://doi.org/10.1137/0404017)) prove the conjecture on the real line via **Double Coverage**; Chrobak and Larmore ([SIAM J. Comput.](https://doi.org/10.1137/0220008)) extend it to all tree metrics. - **1995.** Koutsoupias and Papadimitriou ([J. ACM](https://doi.org/10.1145/210118.210128)) prove the **Work Function Algorithm** is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: *for every metric space there is an online algorithm with competitive ratio $k$.* - **1996.** The same authors verify the conjecture on spaces of $k+2$ points via the dual **2-evader problem** (Inf. Process. Lett. 57). - **2004.** Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points. - **2021.** Coester and Koutsoupias ([ICALP](https://arxiv.org/abs/2102.10474)) give a unifying potential for all known WFA analyses and push the frontier to the circle. - **2023.** Bubeck, Coester, and Rabani ([STOC](https://arxiv.org/abs/2211.05753)) refute the *randomized* analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995. ## Setting Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A **configuration** records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the **movement cost** is the total distance traveled, $$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$ A **request sequence** is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list). A **deterministic online algorithm** $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the **initial configuration**, before any request arrives. Two points about this way of modeling an algorithm: - *Online and deterministic, by construction.* The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices. - *The service constraint.* Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$. Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its **cost** is the total movement along this trajectory: $$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$ For comparison, an **offline schedule** for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The **optimal offline cost** $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$. Finally, $A$ is **$c$-competitive** if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with $$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$ ## Formalization targets ### Goal — the $k$-server conjecture $$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$ The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof. ### Milestones — the known ladder The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm *itself* — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the *randomized* analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms. ## Significance A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences. None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem. ## Difficulty The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server *other than* the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$. ## Formalization scope The Lean model commits to: configurations as functions `Fin k → M` (**labeled** servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions `List M → (Fin k → M)` with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in `ℝ` via `Metric.dist`; the offline optimum as an `sInf` over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as `∃ a, ∀ σ`. Two conventions guard against trivialization. The additive constant is quantified *before* the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ *distinct* points (`Finset.card = k + 1`); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false. Three further definitional layers extend the model. The **work function** `workFunction C₀ σ C` is the `sInf` of (schedule cost + final move to `C`) over schedules serving `σ` from `C₀`, and the **Work Function Algorithm** `WFA` is defined on finite spaces with `k ≥ 1` servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A **tree** is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A **randomized algorithm** is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences. Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about `moveCost`, schedules, and work functions published as reusable platform theorems. ## Selected references - M. Manasse, L. McGeoch, D. Sleator, *Competitive algorithms for server problems*, J. Algorithms 11 (1990). [doi:10.1016/0196-6774(90)90003-W](https://doi.org/10.1016/0196-6774(90)90003-W) - A. Fiat, Y. Rabani, Y. Ravid, *Competitive k-server algorithms*, FOCS 1990. [doi:10.1109/FSCS.1990.89566](https://doi.org/10.1109/FSCS.1990.89566) - M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, *New results on server problems*, SIAM J. Discrete Math. 4 (1991). [doi:10.1137/0404017](https://doi.org/10.1137/0404017) - M. Chrobak, L. Larmore, *An optimal on-line algorithm for k servers on trees*, SIAM J. Comput. 20 (1991). [doi:10.1137/0220008](https://doi.org/10.1137/0220008) - E. Koutsoupias, C. Papadimitriou, *On the k-server conjecture*, J. ACM 42 (1995). [doi:10.1145/210118.210128](https://doi.org/10.1145/210118.210128) - E. Koutsoupias, C. Papadimitriou, *The 2-evader problem*, Inf. Process. Lett. 57(5) (1996), 249–252. - C. Coester, E. Koutsoupias, *Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle*, ICALP 2021. [arXiv:2102.10474](https://arxiv.org/abs/2102.10474) - S. Bubeck, C. Coester, Y. Rabani, *The randomized k-server conjecture is false!*, STOC 2023. [arXiv:2211.05753](https://arxiv.org/abs/2211.05753) - E. Koutsoupias, *The k-server problem* (survey), Computer Science Review 3 (2009). [doi:10.1016/j.cosrev.2009.04.002](https://doi.org/10.1016/j.cosrev.2009.04.002)

62 thms1 active userReviewed
Captain: Shuze Chen

The 4/3 Conjecture for Metric TSPOpen Problem

## Motivation The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The **subtour-elimination relaxation** (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the **integrality gap** of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The **4/3 conjecture** — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades. ## Timeline - **1954.** Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP. - **1970–1971.** Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound". - **1976/1978.** Christofides, and independently Serdyukov, give the $3/2$-approximation: minimum spanning tree plus a matching on odd-degree vertices. - **1980.** Wolsey ([Math. Prog. Study 13](https://doi.org/10.1007/BFb0120913)) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, so the integrality gap is at most $3/2$. Shmoys and Williamson ([IPL 1990](https://doi.org/10.1016/0020-0190(90)90028-V)) rediscover this via a monotonicity property. - **1995.** Goemans ([Math. Programming 69](https://doi.org/10.1007/BF01585563)) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore. - **2011–2014.** For **graph metrics** (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$, and Sebő–Vygen ([Combinatorica 2014](https://arxiv.org/abs/1201.1870)) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class. - **2020–2022.** Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP ([STOC 2021](https://arxiv.org/abs/2007.01409)) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ ([FOCS 2022](https://arxiv.org/abs/2105.10043)), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin. - **Today.** The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding). ## Setting An **instance** on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$, required to be a **metric cost**: symmetric ($c(u,v) = c(v,u)$), zero on the diagonal ($c(v,v) = 0$), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$. Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP. A **tour** visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written `tspOpt c` — is the minimum over all orderings. The **subtour-elimination (Held–Karp) relaxation** replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is **feasible** (`IsHeldKarp x`) when it is symmetric with zero diagonal, has entries in $[0,1]$, gives every city fractional degree two ($\sum_u x(v,u) = 2$), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$. The **Held–Karp bound** `hkValue c` is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always. ## Formalization targets ### Goal — the 4/3 conjecture $$\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.$$ Together with the known lower-bound families this says the integrality gap is exactly $4/3$. The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it). ### Milestones — the known ladder Five results over the same definitions: the relaxation is valid ($\mathrm{LP} \le \mathrm{OPT}$); instance families force the gap arbitrarily close to $4/3$; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement. ## Significance The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound. Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over `Equiv.Perm`, cut constraints over `Finset`, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP. ## Difficulty The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$, and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory. ## Formalization scope The Lean model commits to: cities `Fin n`; costs `c : Fin n → Fin n → ℝ` with `IsMetricCost` (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings `π : Equiv.Perm (Fin n)` traversed cyclically via `finRotate`, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as `sInf` over nonempty, bounded-below sets of reals, so they are genuine minima for `n ≥ 3`. The hypothesis `3 ≤ n` is load-bearing: for `n ≤ 2` the degree-2 constraints are infeasible, `sInf ∅ = 0` by convention, and the bounds would be false — every theorem therefore carries it. Welcome contributions: the milestones in any order — `held_karp_le_opt` is the natural entry point (the tour's incidence vector crosses every cut at least twice); `integrality_gap_lower_bound` needs the three-path instance family and a case analysis on its tours; `tree_doubling_bound` needs spanning trees against the LP; `wolsey_bound` adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ($7/5$), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions. ## Selected references - G. Dantzig, R. Fulkerson, S. Johnson, *Solution of a large-scale traveling-salesman problem*, Oper. Res. 2 (1954). - M. Held, R. Karp, *The traveling-salesman problem and minimum spanning trees*, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971). - N. Christofides, *Worst-case analysis of a new heuristic for the travelling salesman problem*, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978). - L. Wolsey, *Heuristic analysis, linear programming and branch and bound*, Math. Prog. Study 13 (1980). [doi:10.1007/BFb0120913](https://doi.org/10.1007/BFb0120913) - D. Shmoys, D. Williamson, *Analyzing the Held-Karp TSP bound: a monotonicity property with application*, Inf. Process. Lett. 35 (1990). [doi:10.1016/0020-0190(90)90028-V](https://doi.org/10.1016/0020-0190(90)90028-V) - M. Goemans, *Worst-case comparison of valid inequalities for the TSP*, Math. Programming 69 (1995). [doi:10.1007/BF01585563](https://doi.org/10.1007/BF01585563) - A. Sebő, J. Vygen, *Shorter tours by nicer ears*, Combinatorica 34 (2014). [arXiv:1201.1870](https://arxiv.org/abs/1201.1870) - A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved approximation algorithm for metric TSP*, STOC 2021. [arXiv:2007.01409](https://arxiv.org/abs/2007.01409) - A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved bound on the integrality gap of the subtour LP for TSP*, FOCS 2022. [arXiv:2105.10043](https://arxiv.org/abs/2105.10043) - V. Traub, J. Vygen, *Approximation Algorithms for Traveling Salesman Problems*, Cambridge University Press, 2024. [book page](https://www.or.uni-bonn.de/tspbook/book.pdf)

23 thms1 active userReviewed

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me