The Littlewood conjecture
For any two reals, n·‖nα‖·‖nβ‖ gets arbitrarily close to zero.
▸Motivation
Littlewood, around 1930. Here ‖x‖ is the distance to the nearest integer.
For a single α the analogous statement is false — badly approximable numbers exist — so the conjecture asserts that two numbers cannot be badly approximable simultaneously in this multiplicative sense.
Einsiedler, Katok and Lindenstrauss showed in 2006 that the set of exceptional pairs has Hausdorff dimension zero. No individual pair is known to be exceptional, and none is known to satisfy it either for a genuinely irrational pair.
J. E. Littlewood, c. 1930.
▸Lean API
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Order.Filter.AtTopBot.Defs
namespace Conjectura.AN003
/-- For any two reals, `n · ‖nα‖ · ‖nβ‖` gets arbitrarily close to zero, where `‖·‖`
is distance to the nearest integer. Einsiedler, Katok and Lindenstrauss showed in 2006
that the set of exceptions has Hausdorff dimension zero; no pair is known to fail. -/
def goal : Prop :=
∀ α β : ℝ, ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧
∃ p q : ℤ, (n : ℝ) * |(n : ℝ) * α - p| * |(n : ℝ) * β - q| < ε
end Conjectura.AN003▸Definition
This statement is written entirely in arithmetic and standard number systems — there is no specialised vocabulary to define.
▸Related work1
- Invariant measures and the set of exceptions to Littlewood's conjectureEinsiedler, Katok, Lindenstrauss · 2006
Shows the exceptional set has Hausdorff dimension zero.
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem AN003 — The Littlewood conjecture
For any two reals, n·‖nα‖·‖nβ‖ gets arbitrarily close to zero.
## 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 : ∀ α β : ℝ, ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧
∃ p q : ℤ, (n : ℝ) * |(n : ℝ) * α - p| * |(n : ℝ) * β - q| < ε := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.AN003.Statement
namespace Submission
theorem solution : Conjectura.AN003.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.
(none)
## 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.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.