The unrestricted infinite matroid intersection and packing/covering conjectures
Work with infinite matroids in the sense of Bruhn-Diestel-Kriesell-Pendavingh-Wollan. Two matroids on a common ground set satisfy intersection if some independent in both splits as with . Nash-Williams conjectured this for finitary matroids, and Joo proved it for countable ground sets; Bowler and Carmesin formulated the unrestricted Matroid Intersection Conjecture and the packing/covering conjecture (every family has a partition with disjoint spanning sets in each and independent sets in each contraction onto covering ) and showed them related. Joo asked whether intersection holds for two partitional matroids on a countable set. Do every two infinite matroids on a common ground set satisfy intersection, and does every family have a packing/covering partition?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Infinite matroid theory
- Posed by
- Nathan Bowler and Johannes Carmesin (Combinatorica 2015), extending Nash-Williams' intersection conjecture; Joo (2021, Question 1.5) for partitional matroids
- Year posed
- 2015
- Years open
- 11y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 28 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: in ZFC there are a countably infinite set and two self-dual infinite matroids on with for all independent ; the pair has no packing/covering partition, so the infinite matroid packing/covering conjecture is false. Corollary 1.2: the same partitional pair fails intersection, refuting the unrestricted infinite Matroid Intersection Conjecture and answering Joo's Question 1.5 negatively. The examples are neither finitary nor cofinitary, so Nash-Williams' original conjecture for finitary matroids and the cofinitary cases are untouched. The local building block also answers the Bowler-Geschke ZFC question on self-dual uniform matroids (separate entry).
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human-edited). The manuscript is authored 'OpenAI' and names no human author. The family has one manuscript; the construction is formalized in Lean (see verification).
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 and Corollary 1.2 were read against the conjectures as the paper quotes them from Bowler-Carmesin and Joo. formalization.yaml lists ComparatorChallenges/InfiniteMatroid.json with declaration OAI.InfiniteMatroidCounterexample.main in OAI/Combinatorics/InfiniteMatroid/Main.lean (file exists at the pinned commit). Its statement, read here, gives two Mathlib matroids (which allow infinite ground sets with the maximality axiom) on a countable infinite type, both self-dual, with no independent cover of the ground set and no packing/covering partition: the headline disproof. lean/docs/185.md also links InfiniteMatroidCorollaries.json (module OAI.Combinatorics.InfiniteMatroid.Corollaries, file exists, not in the formalization catalogue), whose statement adds that both matroids are partitional and fail intersection, and that the separate covering and packing conjectures fail. Not rebuilt here.
Sources
- Lean proofLean proof (OAI.InfiniteMatroidCounterexample.main)Lean corollaries (partitional intersection, covering, packing)
- CodeOpenAI math release: A Counterexample to the Infinite Matroid Packing/Covering Conjecture
- Problem recordBowler-Carmesin, Matroid intersection, base packing and base covering for infinite matroids