/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilDe Giorgi's conjecture
This file states a conjecture of De Giorgi about entire solutions to $Δ u + u - u^3 = 0$. The conjecture is a rigidity theorem: in spatial dimension $n ≤ 8$, the level sets of bounded solutions which satisfy $∂₁u > 0$ everywhere are hyperplanes. It has been shown that the condition $n ≤ 8$ is sharp.
The main theorems are:
DeGiorgi_le_eight: the conjecture holds in dimension $n ≤ 8$.
DeGiorgi_ge_nine: the conclusion of the conjecture does not hold if $n ≥ 9$.
The cases $1 ≤ n ≤ 8$ are also listed individually to enable partial solutions. The cases $1 ≤ n ≤ 3$ are solved, while $4 ≤ n ≤ 8$ remains open.
Existing results
The case $n = 1$ trivially holds ($u$ is injective since $∂_1 u > 0$).
The case $n = 2$ was proven by Ghoussoub and Gui.
The case $n = 3$ was proven by Ambrosio and Cabré.
The case $4 ≤ n ≤ 8$ was proven under an extra assumption by Savin.
The counterexample for $n ≥ 9$ was proven by Del Pino, Kowalczyk, and Wei.
References
Ghoussoub, Gui, Mathematische Annalen 311 (1998) proves the conjecture for $n = 2$.
Ambrosio, Cabré, Journal of the American Mathematical Society 13 (2000) proves the conjecture for $n = 3$.
Savin, Annals of Mathematics 169 (2009) proves the case $4 ≤ n ≤ 8$ under an additional assumption.
Del Pino, Kowalczyk, Wei, Annals of Mathematics 174 (2011) shows that the condition $n ≤ 8$ is sharp.
open ContDiff Set InnerProductSpace MeasureTheory EuclideanGeometryopen scoped Laplacian
namespace DeGiorgi
variable {n : ℕ} [NeZero n]
The function $u : ℝ^n → ℝ$ is a bounded classical solution to $Δ u + u - u^3 = 0$.
structure IsBoundedSolution (u : ℝ^n → ℝ) : Prop where
regular : ContDiff ℝ 2 u
bounded : ∃ C, ∀ x, |u x| ≤ C
solution : ∀ x, (Δ u x) + u x - (u x) ^ 3 = 0
The first partial derivative of $u : ℝ^n → ℝ$ is strictly positive.
def HasPositiveDeriv (u : ℝ^n → ℝ) : Prop :=
∀ x, 0 < lineDeriv ℝ u x (EuclideanSpace.single 0 1)
The level sets of $u : ℝ^n → ℝ$ are hyperplanes. This is expressed by stating that there exists some affine subspace with rank $n - 1$ which coincides with the level set.
def HasHyperplaneLevelSets (u : ℝ^n → ℝ) : Prop :=
∀ y ∈ range u, ∃ S : AffineSubspace ℝ (ℝ^n),
u⁻¹' {y} = S ∧ Module.finrank ℝ S.direction = n - 1
The conclusion to De Giorgi's conjecture: if $u : ℝ^n → ℝ$ is a bounded classical solution to $Δ u + u - u^3 = 0$ satisfying $∂₁u > 0$ everywhere, then the level sets of $u$ are hyperplanes.
def DeGiorgi_conclusion (n : ℕ) [NeZero n] : Prop :=
∀ u : ℝ^n → ℝ, (IsBoundedSolution u ∧ HasPositiveDeriv u) → HasHyperplaneLevelSets u
De Giorgi's conjecture holds in dimension $n ≤ 8$.
@[category research open, AMS 35]
theorem DeGiorgi_le_eight (hn : n ≤ 8) : (DeGiorgi_conclusion n) := n:ℕinst✝:NeZero nhn:n ≤ 8⊢ DeGiorgi_conclusion n
All goals completed! 🐙
In dimension $n ≥ 9$, the conclusion of De Giorgi's conjecture does not hold.
@[category research solved, AMS 35]
theorem DeGiorgi_ge_nine (hn : n ≥ 9) : ¬(DeGiorgi_conclusion n) := n:ℕinst✝:NeZero nhn:n ≥ 9⊢ ¬DeGiorgi_conclusion n
All goals completed! 🐙
De Giorgi's conjecture trivially holds in dimension $n = 1$.
@[category research solved, AMS 35]
theorem DeGiorgi_one : (DeGiorgi_conclusion 1) := ⊢ DeGiorgi_conclusion 1
intro u u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv u⊢ HasHyperplaneLevelSets u u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv uy:ℝ⊢ y ∈ range u → ∃ S, u ⁻¹' {y} = ↑S ∧ Module.finrank ℝ ↥S.direction = 1 - 1 u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv uy:ℝhy:y ∈ range u⊢ ∃ S, u ⁻¹' {y} = ↑S ∧ Module.finrank ℝ ↥S.direction = 1 - 1
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ ∃ S, u ⁻¹' {u x} = ↑S ∧ Module.finrank ℝ ↥S.direction = 1 - 1
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ u ⁻¹' {u x} = ↑(affineSpan ℝ {x})u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Module.finrank ℝ ↥(affineSpan ℝ {x}).direction = 1 - 1
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ u ⁻¹' {u x} = ↑(affineSpan ℝ {x}) u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ u ⁻¹' (u '' {x}) = {x}
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Function.Injective u
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Function.Injective (u ∘ fun t => EuclideanSpace.single 0 t)u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Function.Surjective fun t => EuclideanSpace.single 0 t
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Function.Injective (u ∘ fun t => EuclideanSpace.single 0 t) u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range ut:ℝ⊢ 0 < deriv (u ∘ fun t => EuclideanSpace.single 0 t) t
u:ℝ^1 → ℝhu_sol:IsBoundedSolution ux:ℝ^1hy:u x ∈ range ut:ℝhu_deriv:0 < lineDeriv ℝ u (EuclideanSpace.single 0 t) (EuclideanSpace.single 0 1)⊢ 0 < deriv (u ∘ fun t => EuclideanSpace.single 0 t) t
u:ℝ^1 → ℝhu_sol:IsBoundedSolution ux:ℝ^1hy:u x ∈ range ut:ℝhu_deriv:0 < lineDeriv ℝ u (EuclideanSpace.single 0 t) (EuclideanSpace.single 0 1)⊢ 0 < deriv (fun x => (fun x => u (EuclideanSpace.single 0 x)) (t + x)) 0
u:ℝ^1 → ℝhu_sol:IsBoundedSolution ux:ℝ^1hy:u x ∈ range ut:ℝhu_deriv:0 < deriv (fun t_1 => u (EuclideanSpace.single 0 t + t_1 • EuclideanSpace.single 0 1)) 0⊢ 0 < deriv (fun x => (fun x => u (EuclideanSpace.single 0 x)) (t + x)) 0
u:ℝ^1 → ℝhu_sol:IsBoundedSolution ux:ℝ^1hy:u x ∈ range ut:ℝhu_deriv:0 < deriv (fun t_1 => u (EuclideanSpace.single 0 t + t_1 • EuclideanSpace.single 0 1)) 0x✝:ℝ⊢ EuclideanSpace.single 0 (t + x✝) = EuclideanSpace.single 0 t + x✝ • EuclideanSpace.single 0 1
All goals completed! 🐙
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Function.Surjective fun t => EuclideanSpace.single 0 t exact fun t ↦ ⟨t 0, u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range ut:ℝ^1⊢ (fun t => EuclideanSpace.single 0 t) (t.ofLp 0) = t u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range ut:ℝ^1i✝:Fin 1⊢ ((fun t => EuclideanSpace.single 0 t) (t.ofLp 0)).ofLp i✝ = t.ofLp i✝; u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range ut:ℝ^1i✝:Fin 1⊢ (if i✝ = 0 then t.ofLp 0 else 0) = t.ofLp i✝; All goals completed! 🐙⟩
u:ℝ^1 → ℝhu_sol:IsBoundedSolution uhu_deriv:HasPositiveDeriv ux:ℝ^1hy:u x ∈ range u⊢ Module.finrank ℝ ↥(affineSpan ℝ {x}).direction = 1 - 1 All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 2$.
@[category research solved, AMS 35]
theorem DeGiorgi_two : (DeGiorgi_conclusion 2) := ⊢ DeGiorgi_conclusion 2
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 3$.
@[category research solved, AMS 35]
theorem DeGiorgi_three : (DeGiorgi_conclusion 3) := ⊢ DeGiorgi_conclusion 3
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 4$.
@[category research open, AMS 35]
theorem DeGiorgi_four : (DeGiorgi_conclusion 4) := ⊢ DeGiorgi_conclusion 4
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 5$.
@[category research open, AMS 35]
theorem DeGiorgi_five : (DeGiorgi_conclusion 5) := ⊢ DeGiorgi_conclusion 5
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 6$.
@[category research open, AMS 35]
theorem DeGiorgi_six : (DeGiorgi_conclusion 6) := ⊢ DeGiorgi_conclusion 6
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 7$.
@[category research open, AMS 35]
theorem DeGiorgi_seven : (DeGiorgi_conclusion 7) := ⊢ DeGiorgi_conclusion 7
All goals completed! 🐙
De Giorgi's conjecture holds in dimension $n = 8$.
@[category research open, AMS 35]
theorem DeGiorgi_eight : (DeGiorgi_conclusion 8) := ⊢ DeGiorgi_conclusion 8
All goals completed! 🐙
end DeGiorgi