theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← erdos_1.variants.lb
⌘↵
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 /-- Erdős and Moser [Er56] proved $$ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. $$ [Er56] Erdős, P., _Problems and results in additive number theory_. Colloque sur la Th\'{E}orie des Nombres, Bruxelles, 1955 (1956), 127-137. -/ @[category research solved, AMS 5 11] theorem erdos_1.variants.lb : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)), ∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N), (1 / 4 - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N := by sorry
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…