halls_conjecture
Provedalgebraic-geometrynumber-theory
Hall's conjecture (1971): If y² = x³ + k is satisfied by positive integers x, y, then |x| < C|y|^{2/3+ε} for any ε > 0. Or equivalently, the ABC conjecture implies |x| ≥ C|k|^{1/(3+ε)} for any integral point (x,y) of high magnitude. Connected to Lang's conjecture on Mordell curves.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem halls_conjecture :
∀ eps : ℝ, 0 < eps →
∃ C : ℝ, 0 < C ∧
∀ x y : ℤ, 0 < x → 0 < y → y ^ 2 = x ^ 3 + 1 →
x ≤ C * y ^ (2/3 + eps) := by
sorrySource