Mahler's 3/2 Problem

Reference: Wikipedia

theorem Mahler32.mahler_conjecture (x : ℝ) (hx : Mahler32.IsZNumber✝ x) : False

The Mahler Conjecture states that there are no Z-numbers.

theorem Mahler32.mahler_conjecture.variants.consequence (H : ∀ (x : ℝ), Mahler32.IsZNumber✝ x → False) : 1 / 2 < Mahler32.Ω✝ (3 / 2)

If Mahler's conjecture is true, i.e. there are no Z-numbers, then Ω(3/2) exceeds 1/2.

theorem Mahler32.mahler_conjecture.variants.flatto_lagarias_pollington (p q : ℕ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : p.Coprime q) (hpq' : q < p) : 1 / ↑p < Mahler32.Ω✝ (↑p / ↑q)

It is known that for all rational p/q > 1 in lowest terms, we have Ω(p/q) > 1/p.