Aftermath bot: New page: the strong thin-tree conjecture, family 174, with public follow-ups

2026-10-19T22:21:19Z

New page: the strong thin-tree conjecture, family 174, with public follow-ups

New page

'''The strong thin-tree conjecture''' predicts a universal constant ''C'' such that every ''k''-edge-connected multigraph has a spanning tree using at most a ''C''/''k'' fraction of the edges of every cut. Two manuscripts in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), both dated 23 September 2026, claim the conjecture and a deterministic polynomial-time construction of such trees. The collection includes a Lean formalization of both statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introductions of the manuscripts:
** Goddyn's thin tree conjecture asks whether sufficiently high edge connectivity forces an ε-thin spanning tree for every ε > 0; the strong form with the rate ''C''/''k'' is distinguished explicitly by Anari and Oveis Gharan. The order 1/''k'' is necessary, as two vertices joined by ''k'' parallel edges show.
** Asadpour, Goemans, Mądry, Oveis Gharan and Saberi used maximum-entropy distributions on spanning trees to obtain an ''O''(log ''n''/log log ''n'') approximation for the asymmetric traveling salesman problem, and their rounding also gives thin trees at the corresponding scale. Oveis Gharan and Saberi obtained inverse-connectivity bounds for planar graphs and graphs of bounded orientable genus.
** Anari and Oveis Gharan introduced effective-resistance-reducing flows and locally connected hierarchies and proved the existence of poly(log log ''n'')/''k''-thin trees; the manuscripts describe their method as the principal geometric foundation of the proof. Klein and Olver treated every prescribed laminar family of cuts, and Klein, Olver and Yeoh constructed a tree crossing every cut of size less than (1 + 1/40)''k'' at most 88 times. Constant-factor approximation for the asymmetric traveling salesman problem had already been obtained by Svensson, Tarnawski and Végh, and improved by Traub and Vygen, by other methods.

== The original results ==
* '''Claim.''' Theorem 1.1 of ''The strong thin tree conjecture'' states that there is a universal constant ''C'' > 0 such that, for every integer ''k'' ≥ 1, every finite ''k''-edge-connected loopless multigraph with at least two vertices has a spanning tree crossing every cut in at most ''C''/''k'' times the number of edges of that cut. Theorem 1.1 of ''A polynomial-time construction of strong thin trees'' states that such a tree is returned by a deterministic algorithm in time polynomial in the binary input length, whether the edges are listed explicitly or the multiplicities of parallel edges are encoded in binary. The second manuscript also derives a rounding of fractional cut covers to spanning trees in their support with cut loads and total cost bounded by constant multiples of the fractional quantities.
* ''Method, as described:'' a large packing of edge-disjoint spanning trees is maintained through a sequence of sparsifications that reduce cut sizes and packing size by almost the same factor. Each step extracts a large packing on edges of small resistance with respect to a matrix built from the locally connected hierarchies of Anari and Oveis Gharan, and then selects about half of the edges by the theorem of Marcus, Spielman and Srivastava applied to two stacked vector representations, one controlling cuts and one certifying tree packing. The algorithmic manuscript replaces the existential steps by an ellipsoid-method computation over a larger cone of metric tests, exact rational data and a constructive matrix signing that follows Ezeunala and Jiang.
* '''Sources.''' The manuscripts [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-strong-thin-tree-conjecture-September-23-2026 The strong thin tree conjecture] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026 A polynomial-time construction of strong thin trees] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/174.md scope note] states that the formalization gives one absolute constant ''C'' > 0 such that every finite loopless ''k''-edge-connected multigraph with at least two vertices has a spanning tree crossing each nontrivial cut at most ''C''/''k'' times the original cut size, with parallel edges kept distinct and no numerical value of ''C'' asserted, and separately a deterministic polynomial-time algorithm with such a constant, whose input may encode parallel-edge multiplicities in binary. The Comparator statements are <code>StrongThinTree.lean</code> and <code>AlgorithmicThinTrees.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": both the existence theorem and the polynomial-time algorithm are stated, and binary multiplicities are genuinely encoded in binary. It notes that polynomial time is defined through a custom multi-stack machine model rather than Mathlib's notion, which it considers faithful. It records sandboxed Comparator passes for <code>StrongThinTree</code> and <code>AlgorithmicThinTrees</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-08
| [https://github.com/th1enq/ATSP/tree/965bcc54503e17b80e5c8095f256a58f2f81fa1c th1enq/ATSP] (GitHub)
| Uses (conditional on the result)
| A C++ research artifact for the chain from Held–Karp feasibility to constant supported thin trees and constant-factor approximation of the bottleneck asymmetric traveling salesman problem. It cites the OpenAI result together with An, Kleinberg and Shmoys, and states that the OpenAI construction is not reimplemented: exact and heuristic thin-tree oracles stand in for it, while the An–Kleinberg–Shmoys rounding is implemented and tested exhaustively for ''n'' = 4 and 5.
| Repository.
|-
| 2026-10-10 || cert-machine, openai/math lane K: [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/StrongThinTree.json StrongThinTree] (run 38019899278) and [https://github.com/carlostoledo1891/cert-machine/blob/3e3937cd5e4a4cacd451447c4ed8033eb0340521/corpus/openai-math/kernel-runs/38051470892/AlgorithmicThinTrees.json AlgorithmicThinTrees] (run 38051470892) || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept both solutions, in 613 s and 1,795 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists neither challenge, so both were accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_432.json referee review] of the polynomial-time manuscript in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
| Review (AI-assisted audit)
| Reports no gap and states that the reviewer read the whole manuscript except the fractional-rounding corollary. Its one minor note is that the transfer from the companion's cut geometry to the metric-cone polytope is given as a proof sketch that takes the scalar accounting and case constructions from the companion's appendix without repeating them, so the final hierarchy bound stands only if those companion arguments are correct; the reviewer did not re-verify them.
| Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The strong thin-tree conjecture - Revision history

Aftermath bot: New page: the strong thin-tree conjecture, family 174, with public follow-ups