The infinite matroid intersection and packing/covering conjectures

The infinite matroid intersection and packing/covering conjectures extend Edmonds' matroid intersection theorem and the Nash-Williams packing and covering theorems to infinite matroids in the sense of Bruhn, Diestel, Kriesell, Pendavingh and Wollan. Bowler and Carmesin formulated the packing/covering conjecture and related it to the infinite matroid intersection conjecture. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims counterexamples to both in ZFC, using two self-dual partitional matroids on a countably infinite ground set. The collection includes a Lean formalization of this statement. This page summarizes the published claim 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 introduction of the manuscript:
- The axioms of Bruhn, Diestel, Kriesell, Pendavingh and Wollan give an infinite matroid theory with restriction, contraction and duality. Bowler and Carmesin formulated the packing/covering conjecture, proved its equivalence with the unrestricted infinite matroid intersection conjecture, and formulated separate covering and packing conjectures.
- Bowler and Geschke developed a basis criterion for infinite uniform matroids and constructed countable self-dual examples under Martin's axiom for countable posets; whether such a matroid exists in ZFC was left open, and Gollin and Joó record ZFC existence of a uniform matroid of infinite rank and corank as open. Joó proved an intersection theorem for an arbitrary matroid paired with a direct sum of finitely many uniform matroids and asked whether intersection holds for two partitional matroids on a countable ground set.

The original result

Claim. Theorem 1.1 of A Counterexample to the Infinite Matroid Packing/Covering Conjecture states that in ZFC there are a countably infinite set E and two self-dual infinite matroids on E whose independent sets never cover E together, and that this pair has no packing/covering partition, so the packing/covering conjecture is false. Corollary 1.2 states that the same pair consists of partitional matroids and does not satisfy intersection, which refutes the unrestricted infinite matroid intersection conjecture and answers Joó's question negatively. The manuscript also deduces that the separate covering and packing conjectures are false. It states that the examples are neither finitary nor cofinitary, so Nash-Williams' original finitary conjecture is not addressed.
Method, as described: a local construction in ZFC of a self-dual uniform matroid on a countable set whose bases satisfy an additional ordinal inequality, which the manuscript says also answers the existence questions of Bowler–Geschke and Gollin–Joó; copies of it are placed along a doubly infinite path so that the inequality obstructs independent coverings, and the two matroids are countable direct sums of these copies.
Sources. The manuscript A Counterexample to the Infinite Matroid Packing/Covering Conjecture at commit 1581d4c.
Formalization, as described by the repository. The scope note states that the formalization constructs two self-dual partitional matroids on one countably infinite ground set that admit neither an independent covering nor a packing/covering partition, that the same pair has no intersection witness, and that separate formalized consequences refute the individual covering and packing conjectures, in ordinary set theory with Choice and without a finitary restriction. The Comparator statements are InfiniteMatroid.lean and InfiniteMatroidCorollaries.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 20 October 2026)
2026-10-07	VolMax-Studio/p10-openai-math-verification-pilot (GitHub)	Verification (formal)	An independent execution of the formal verification path for the main theorem in a separately pinned environment, reporting provenance binding, an independent Lean build, Comparator verification, negative controls and dependency integrity as passing, with only the standard axioms.	The README states that this is not a claim that the manuscript has been independently verified, nor a reproduction of OpenAI's original verifier run.
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit `c76f1e4`, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "full". Its review note states that the main challenge gives two self-dual matroids on a countable infinite set with no covering and no packing/covering partition, that the corollary challenge adds partitionality and the failure of intersection, answering Joó's question, as well as the separate covering and packing counterexamples, and that the conjecture predicates are written out by hand on top of Mathlib's infinite matroids and look standard. It records sandboxed Comparator passes for both challenges.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10	cert-machine, openai/math lane K: run 38019899278 for InfiniteMatroid and InfiniteMatroidCorollaries	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept both solutions, in 166 s and 183 s. The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions (time-outs, memory, errors) lists neither `InfiniteMatroid` nor `InfiniteMatroidCorollaries`, so both were accepted by con-leche and by Lean's official kernel.	Development journal.

Notes

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