Prove2Me

rota_basis_conjecture

Disproved

by tianyipeng · May 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsconjecturelinear-algebramatroid-theorymatroids

Rota's basis conjecture (1989): Given n bases B₁,...,Bₙ of an n-dimensional vector space V, there exists a system of distinct representatives (one from each basis) forming a basis. Proved for n ≤ 3 and special cases; general n is open.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem rota_basis_conjecture (n : ℕ) (hn : 1 ≤ n)
    (V : Type*) [AddCommGroup V] [Module ℝ V]
    (hdim : Module.finrank ℝ V = n)
    (bases : Fin n → Fin n → V)
    (hbases : ∀ i : Fin n, LinearIndependent ℝ (bases i)) :
    ∃ sigma : Fin n → Fin n,
      Function.Injective sigma ∧
      LinearIndependent ℝ (fun i => bases i (sigma i)) := by
  sorry
Source
https://en.wikipedia.org/wiki/Rota%27s_basis_conjecture

View graph