# Counterexamples to infinite matroid intersection and packing/covering

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Counterexample to the Infinite Matroid Packing/Covering Conjecture](../../preprints/A-Counterexample-to-the-Infinite-Matroid-Packing-Covering-Conjecture-September-24-2026/paper.pdf)

## Scope

The infinite matroid packing/covering conjecture predicts a partition of a common ground set into parts admitting the corresponding packing and covering. 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. The same pair has no intersection witness, so it also refutes the unrestricted infinite matroid intersection conjecture.

Separate formalized consequences give counterexamples to the individual covering and packing conjectures. The construction is in ordinary set theory with Choice and assumes no finitary restriction on the matroids.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Infinite matroid packing/covering counterexample | [InfiniteMatroid.lean](../ComparatorChallenges/InfiniteMatroid.lean) |
| Partitional intersection, covering, and packing counterexamples | [InfiniteMatroidCorollaries.lean](../ComparatorChallenges/InfiniteMatroidCorollaries.lean) |