Rotas Basis Conjecture

### What is the conjecture

Let $M$ be a matroid of rank $n$ with $n$ disjoint bases $B_1, B_2, \ldots, B_n$. Then there exist $n$ disjoint bases $C_1, C_2, \ldots, C_n$ such that each $C_i$ contains exactly one element from each base $B_j$. Equivalently, the elements of these $n$ bases can be arranged into an $n \times n$ matrix where both the rows and columns form bases of $M$.

**Sources:**
- https://en.wikipedia.org/wiki/Rota%27s_basis_conjecture, https://www.sciencedirect.com/science/article/abs/pii/S0196885823001112, https://epubs.siam.org/doi/10.1137/060655596, https://arxiv.org/abs/2107.07024, http://www.openproblemgarden.org/op/rotas_basis_conjecture

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

Mathlib lacks comprehensive matroid theory infrastructure. While basic set-theoretic foundations exist, a complete formalization would require implementing matroid definitions, basis properties, and disjointness constraints. The conjecture's statement is mathematically precise and can be formalized once matroid theory is adequately developed in Lean, requiring significant new definitions and lemmas about matroid independence systems and basis rearrangements.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.