lehmer_mahler_conjecture

Disproved

by tianyipeng · May 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebragraph-theorynumber-theorypolynomials

Lehmer's conjecture (1933): The Mahler measure of any non-cyclotomic irreducible polynomial over ℤ is at least Lehmer's number ≈ 1.17628. This would bound the smallest algebraic integers in terms of their degree.

Preamble

import Mathlib

Formal statement

import Mathlib

-- Lehmer's conjecture: the Mahler measure of a non-cyclotomic irreducible polynomial
-- over ℤ is at least Lehmer's number ≈ 1.1762808...
-- (the Mahler measure of x^10 + x^9 - x^7 - x^6 - x^5 - x^4 - x^3 + x + 1)
-- Formalized: if p : Polynomial ℤ is irreducible, monic, non-cyclotomic, then M(p) ≥ c
theorem lehmer_mahler_conjecture :
    ∃ c : ℝ, 1 < c ∧
    ∀ p : Polynomial ℤ, Irreducible p → p.Monic →
      (¬∃ n : ℕ, 1 ≤ n ∧ p ∣ (Polynomial.cyclotomic n ℤ)) →
      c ≤ (Finset.univ.prod (fun z : p.roots.toFinset =>
        max 1 (Complex.normSq z))) := by
  sorry

Source

https://en.wikipedia.org/wiki/Lehmer%27s_conjecture

View graph