Hall's conjecture

HallIneqdef

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

HallConjectureExpdef

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

hall_conjecturetheorem

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

theorem hall_conjecture : HallConjectureExp 2⁻¹ := by
  sorry

elkies_boundtheorem

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

danilovtheorem

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_hall_conjecturetheorem

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

goaldef

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

def goal : Prop :=
  HallConjectureExp 2⁻¹

From Mathlib

Analysis.SpecialFunctions.Pow.Real

import Conjectura.Problems.WP0016.Statement · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `Wikipedia/Hall.lean`. The problem is catalogued at https://en.wikipedia.org/wiki/Hall%27s_conjecture. LOCKED: solvers cannot modify this file.

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

Full credits