Hall's conjecture

There exists a positive number $C$ such that for any integer $x, y$ with $y^2 \ne x^3$, $|y^2 - x^3| > C \sqrt{|x|}$.

References:

• Wikipedia
• L. Danilov, The Diophantine equation $x^3 - y^2 = k$ and Hall's conjecture, Mathematical notes of the Academy of Sciences of the USSR 32 (1982): 617-618

def Hall.HallIneq (C e : ℝ) : Prop

Equations

• Hall.HallIneq C e = ∀ (x y : ℤ), y ^ 2 ≠ x ^ 3 → ↑|y ^ 2 - x ^ 3| > C * |↑x| ^ e

def Hall.HallConjectureExp (e : ℝ) : Prop

Equations

• Hall.HallConjectureExp e = ∃ C > 0, Hall.HallIneq C e

theorem Hall.hall_conjecture : HallConjectureExp 2⁻¹

Original Hall's conjecture with exponent $1/2$.

theorem Hall.elkies_bound (C : ℝ) : HallIneq C 2⁻¹ → C < 215e-4

Elkies' example $(x, y) = (5853886516781223, 447884928428402042307918)$ shows that such $C$ must be less than $0.0215$. Note that simple linarith does not work here.

theorem Hall.danilov (δ : ℝ) (h : δ > 0) : ¬HallConjectureExp (2⁻¹ + δ)

Danilov proved that one cannot replace the exponent $1/2$ with larger number. In other words, for any $\delta > 0$, there is no positive constant $C$ such that $|y^2 - x^3| > C |x| ^ {1/2 + \delta}$ for all integers $x, y$ with $y^2 \ne x^3$.

theorem Hall.weak_hall_conjecture (ε : ℝ) (hε : ε > 0) : HallConjectureExp (2⁻¹ - ε)

Weak form of Hall's conjecture: relax the exponent from $1/2$ to $1/2 - \varepsilon$.