Hall's conjecture

Conjectura.Problems.WP0016.Statement

/-
Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors
-/
import Mathlib.Analysis.SpecialFunctions.Pow.Real

/-! # Hall's conjecture

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `Wikipedia/Hall.lean`. The problem is catalogued at [https://en.wikipedia.org/wiki/Hall%27s_conjecture](https://en.wikipedia.org/wiki/Hall%27s_conjecture).

LOCKED: solvers cannot modify this file.
-/

open Real

namespace Conjectura.WP0016

def HallIneq (C : ℝ) (e : ℝ) : Prop :=
  ∀ x y : ℤ, y ^ 2 ≠ x ^ 3 → |y ^ 2 - x ^ 3| > C * (|x| : ℝ) ^ e

def HallConjectureExp (e : ℝ) : Prop := ∃ C : ℝ, C > 0 ∧ HallIneq C e


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

theorem hall_conjecture : HallConjectureExp 2⁻¹ := by
  sorry

/--
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 elkies_bound (C : ℝ) : HallIneq C 2⁻¹ → C < 0.0215 := by
  intro h
  by_cases hC : C ≤ 0
  · linarith
  · rw [HallIneq] at h
    specialize h 5853886516781223 447884928428402042307918
    simp at h
    have h1 : 76510695 < (5853886516781223 : ℝ) ^ (2 : ℝ)⁻¹ := by
      norm_num
      rw [← sqrt_eq_rpow]
      refine lt_sqrt_of_sq_lt ?_
      norm_num
    have h2 : C * 76510695 < 1641843 := by
      nlinarith
    linarith

/--
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 danilov (δ : ℝ) (h : δ > 0) : ¬ HallConjectureExp (2⁻¹ + δ) := by sorry

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

theorem weak_hall_conjecture (ε : ℝ) (hε : ε > 0) : HallConjectureExp (2⁻¹ - ε) := by
  sorry

/-- Original Hall's conjecture with exponent $1/2$. -/
def goal : Prop :=
  HallConjectureExp 2⁻¹

end Conjectura.WP0016