weil_height_conjecture
Disprovedalgebraalgebraicnumbertheorycombinatoricsgraph-theoryheightsnumber-theorynumbertheoryopenproblemproved
Northcott property and Weil height: Sets of algebraic numbers with bounded degree and bounded Weil height are finite. This is the Northcott property (proved). Various refinements about the distribution of heights are open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem weil_height_conjecture (K : Type*) [Field K] [NumberField K]
(d : ℕ) (hd : 1 ≤ d) :
∀ eps : ℝ, 0 < eps →
{x : K | ∃ (h : ℝ), 0 ≤ h ∧ h ≤ d ∧
∀ (y : K), x ≠ y → True}.Finite := by
sorrySource