theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← erdos_1.variants.least_N_9
⌘↵
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 /-- The minimal value of $N$ such that there exists a sum-distinct set with nine elements is $161$. https://oeis.org/A276661 -/ @[category research solved, AMS 5 11] theorem erdos_1.variants.least_N_9 : IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 9 } 161 := by sorry
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…