theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← erdos_90.variants.sawin_explicit
⌘↵
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 /-- **Sawin's explicit exponent.** The constructive disproof can be realised with $c \ge 0.014114$ (absorbing the implicit constant $C$ of Sawin's Theorem 1 into a slightly smaller exponent for all large enough $n$). Reference: Theorem 1 of Sawin, [arXiv:2605.20579](https://arxiv.org/abs/2605.20579) (2026). -/ @[category research solved, AMS 52] theorem erdos_90.variants.sawin_explicit : {n : ℕ | (n : ℝ) ^ (1.014114 : ℝ) ≤ (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…