VibeMathedMath problems solved with AI

The unrestricted infinite matroid intersection and packing/covering conjectures

Work with infinite matroids in the sense of Bruhn-Diestel-Kriesell-Pendavingh-Wollan. Two matroids M,NM,N on a common ground set EE satisfy intersection if some JJ independent in both splits as J=JM⊔JNJ=J_M\sqcup J_N with clM(JM)∪clN(JN)=E\mathrm{cl}_M(J_M)\cup\mathrm{cl}_N(J_N)=E. 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 E=P⊔CE=P\sqcup C with disjoint spanning sets in each Mi↾PM_i\restriction P and independent sets in each contraction onto CC covering CC) 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 EE and two self-dual infinite matroids M0,M1M_0,M_1 on EE with I0∪I1≠EI_0\cup I_1\ne E for all independent I0,I1I_0,I_1; 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 I0∪I1I_0\cup I_1 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

Changelog1 change

Discussion