Lehmer's Mahler measure problem

Conjecture · lehmer_mahler_measure_problem

Let M(f) denote the Mahler measure of f. There exists a constant μ>1 such that for any f(x)∈ℤ[x], M(f)>1 → M(f)≥μ.

Formal statement · Lean 4.lean

theorem lehmer_mahler_measure_problem :
    ∃ μ : ℝ, ∀ f : ℤ[X],
      μ > 1 ∧ (mahlerMeasureZ f > 1 → mahlerMeasureZ f ≥ μ) := by
  sorry

Proof. sorry

Nobody has tried yet.