Back to Problems

Invariant_subspace_problem_finite_dimensional

Specification

Every (bounded) linear operator `T : H → H` on a finite-dimensional linear space `H` of dimension at least 2 has a non-trivial (closed) `T`-invariant subspace. This can be solved using the Jordan normal form, which is [not yet in mathlib](https://leanprover-community.github.io/undergrad_todo.html).

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem Invariant_subspace_problem_finite_dimensional [Module ℂ H] (h : FiniteDimensional ℂ H)
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T)
ID: Wikipedia__InvariantSubspaceProblem__Invariant_subspace_problem_finite_dimensional
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.