← problemsWP0016openMathematics/ Number theory

Hall's conjecture

How close can a perfect square get to a perfect cube? Hall conjectured that $|y^2 - x^3| > C\,|x|^{1/2}$ for some constant $C>0$ and all integers with $y^2 \ne x^3$ — so the gap cannot be much smaller than the square root of $x$ .

▸Motivation

Marshall Hall Jr., 1971. The question is how nearly a cube can be a square: given integers $x, y$ with $y^2 \ne x^3$ , how small can $|y^2 - x^3|$ be relative to $x$ ?

Hall's original conjecture is the exponent $1/2$ , formalized here. It is known to be false as stated for exponents above $1/2$ — Danilov exhibited solutions with $|y^2-x^3| \ll |x|^{1/2}$ — which is why the weaker Hall conjecture with exponent $1/2 - \varepsilon$ is the version usually quoted today. The original therefore sits in an unusual position: widely believed to fail, and not disproved.

It follows from the abc conjecture in the weakened form, which is one of the standard illustrations of how much abc would buy.

Adapted from formal-conjectures, Wikipedia/Hall.lean. Catalogued at https://en.wikipedia.org/wiki/Hall%27s_conjecture.

▸Lean API

import Mathlib.Analysis.SpecialFunctions.Pow.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$. -/
def goal : Prop :=
  HallConjectureExp 2⁻¹

end Conjectura.WP0016

▸Definition2

HallConjectureExpConjectura.WP0016.HallConjectureExp: def HallConjectureExp (e : ℝ) : Prop := ∃ C : ℝ, C > 0 ∧ HallIneq C e
HallIneqConjectura.WP0016.HallIneq: def HallIneq (C : ℝ) (e : ℝ) : Prop := ∀ x y : ℤ, y ^ 2 ≠ x ^ 3 → |y ^ 2 - x ^ 3| > C * (|x| : ℝ) ^ e

Download the Lean definitions

▸Related work2

Hall's conjecture—
The catalogue entry, with references and status.
formal-conjecturesThe Formal Conjectures Authors (Google DeepMind) · 2025
Source of the Lean formalization adapted here.

▸For your AI

Download as .md

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem WP0016 — Hall's conjecture

How close can a perfect square get to a perfect cube? Hall conjectured that $|y^2 - x^3| > C\,|x|^{1/2}$ for some constant $C>0$ and all integers with $y^2 \ne x^3$ — so the gap cannot be much smaller than the square root of $x$.

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : Conjectura.WP0016.goal := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.WP0016.Statement

namespace Submission

theorem solution : Conjectura.WP0016.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### HallConjectureExp



```lean
Conjectura.WP0016.HallConjectureExp
-- unfolds to:
def HallConjectureExp (e : ℝ) : Prop := ∃ C : ℝ, C > 0 ∧ HallIneq C e
```
Defined in this corpus.

### HallIneq



```lean
Conjectura.WP0016.HallIneq
-- unfolds to:
def HallIneq (C : ℝ) (e : ℝ) : Prop :=
  ∀ x y : ℤ, y ^ 2 ≠ x ^ 3 → |y ^ 2 - x ^ 3| > C * (|x| : ℝ) ^ e
```
Defined in this corpus.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.

Submissions are not open yet

Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.

The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.

Maintain a subject area Download the Lean for this problem

The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.

Discussion

Nothing yet.