The invariant subspace problem
Does every bounded operator on a Hilbert space have a non-trivial closed invariant subspace?
▸Motivation
Open since around 1950 and the most famous unsolved problem in operator theory.
Enflo constructed a counterexample on a general Banach space in 1975 (published 1987), and Read gave one on ℓ¹. The Hilbert space case — the one everybody wants — remains open, and the Banach counterexamples exploit structure Hilbert spaces do not have.
Open since c. 1950. Banach case settled negatively by Enflo, 1975/1987.
▸Lean API
import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
namespace Conjectura.AN009
/-- Does every bounded operator on an infinite-dimensional separable complex Hilbert
space have a non-trivial closed invariant subspace? Enflo settled the Banach space
case negatively in 1975; the Hilbert case is open. -/
def goal : Prop :=
∀ (H : Type) [NormedAddCommGroup H] [NormedSpace ℂ H] [CompleteSpace H],
(∃ f : ℕ → H, Dense (Set.range f)) → ¬ FiniteDimensional ℂ H →
∀ T : H →L[ℂ] H, ∃ S : Submodule ℂ H,
S ≠ ⊥ ∧ S ≠ ⊤ ∧ IsClosed (S : Set H) ∧ ∀ x ∈ S, T x ∈ S
end Conjectura.AN009▸Definition9
- NormedAddCommGroupNormedAddCommGroup
class
- NormedSpaceNormedSpace
class
- CompleteSpaceCompleteSpace
class
- DenseDense
def
- rangeSet.range
def
- FiniteDimensionalFiniteDimensional
abbrev
- SubmoduleSubmodule
structure
- IsClosedIsClosed
def
- SetSet
abbrev
▸Related work1
- On the invariant subspace problem for Banach spacesPer Enflo · 1987
The negative answer for general Banach spaces; the Hilbert case is untouched by it.
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem AN009 — The invariant subspace problem
Does every bounded operator on a Hilbert space have a non-trivial closed invariant subspace?
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution : ∀ (H : Type) [NormedAddCommGroup H] [NormedSpace ℂ H] [CompleteSpace H], ... := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.AN009.Statement
namespace Submission
theorem solution : Conjectura.AN009.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
### NormedAddCommGroup
class
```lean
NormedAddCommGroup
```
Defined in Mathlib.
### NormedSpace
class
```lean
NormedSpace
```
Defined in Mathlib.
### CompleteSpace
class
```lean
CompleteSpace
```
Defined in Mathlib.
### Dense
def
```lean
Dense
```
Defined in Mathlib.
### range
def
```lean
Set.range
```
Defined in Mathlib.
### FiniteDimensional
abbrev
```lean
FiniteDimensional
```
Defined in Mathlib.
### Submodule
structure
```lean
Submodule
```
Defined in Mathlib.
### IsClosed
def
```lean
IsClosed
```
Defined in Mathlib.
### Set
abbrev
```lean
Set
```
Defined in Mathlib.
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Submissions are not open yet
Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.
The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.