theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← erdos_90.variants.polynomial_lower_bound
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
12 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- **Constructive form of the disproof.** There is an absolute constant $c > 0$ such that infinitely many $n$ admit a configuration realising at least $n^{1+c}$ unit distances. This is the qualitative content of Theorem 1.1 of Alon–Bloom–Gowers–Litt–Sawin–Shankar– Tsimerman–Wang–Matchett Wood, [*Remarks on the disproof of the unit distance conjecture*](https://arxiv.org/abs/2605.20695) (2026). An explicit bound $c \ge 0.014114$ is given by Sawin, [*An explicit lower bound for the unit distance problem*](https://arxiv.org/abs/2605.20579) (2026); see `erdos_90.variants.sawin_explicit` below. -/ @[category research solved, AMS 52] theorem erdos_90.variants.polynomial_lower_bound : ∃ c > (0 : ℝ), {n : ℕ | (n : ℝ) ^ (1 + c) ≤ (maxUnitDistances n : ℝ)}.Infinite := by sorry
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…