/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilErdős Problem 1
Reference: erdosproblems.com/1
@[expose] public sectionopen Filteropen scoped Topology Realnamespace Erdos1A finite set of naturals $A$ is said to be a sum-distinct set for $N \in \mathbb{N}$ if $A\subseteq{1, ..., N}$ and the sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$
abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop :=
A ⊆ Finset.Icc 1 N ∧ (fun (⟨S, _⟩ : A.powerset) => S.sum id).InjectiveIf $A\subseteq{1, ..., N}$ with $|A| = n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ then $$ N \gg 2 ^ n. $$
This conjecture is false. A machine-checked disproof constructs sum-distinct sets for which $N / 2^n$ tends to zero.
@[category research solved, AMS 5 11, formal_proof using lean4 at
"https://github.com/tadamcz/erdos1/blob/0e395153306f34b3829d118b85bdd704136f2843/Erdos1/Resolutions/Erdos1_219usd_38h.lean#L2419"]
theorem erdos_1 : ¬ ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ) (_ : IsSumDistinctSet A N),
N ≠ 0 → C * 2 ^ A.card < N := ⊢ ¬∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N
All goals completed! 🐙The trivial lower bound is $N \gg 2^n / n$.
N:ℕA:Finset ℕx✝:IsSumDistinctSet A NhN:N ≠ 0hA1:A ⊆ Finset.Icc 1 NhA2:Function.Injective fun x ↦
match x with
| ⟨S, property⟩ => S.sum idkey:2 ^ A.card ≤ A.card * N + 1hc:A.card ≠ 0⊢ 1 / 3 * 2 ^ A.card < ↑N * ↑A.card
nlinarith [show (2 : ℝ) ^ A.card ≤ ↑A.card * ↑N + 1 from N:ℕA:Finset ℕx✝:IsSumDistinctSet A NhN:N ≠ 0hA1:A ⊆ Finset.Icc 1 NhA2:Function.Injective fun x ↦
match x with
| ⟨S, property⟩ => S.sum idkey:2 ^ A.card ≤ A.card * N + 1hc:A.card ≠ 0⊢ 2 ^ A.card ≤ ↑A.card * ↑N + 1 All goals completed! 🐙,
show (1 : ℝ) ≤ ↑A.card from N:ℕA:Finset ℕx✝:IsSumDistinctSet A NhN:N ≠ 0hA1:A ⊆ Finset.Icc 1 NhA2:Function.Injective fun x ↦
match x with
| ⟨S, property⟩ => S.sum idkey:2 ^ A.card ≤ A.card * N + 1hc:A.card ≠ 0⊢ 1 ≤ ↑A.card All goals completed! 🐙,
show (1 : ℝ) ≤ (N : ℝ) from N:ℕA:Finset ℕx✝:IsSumDistinctSet A NhN:N ≠ 0hA1:A ⊆ Finset.Icc 1 NhA2:Function.Injective fun x ↦
match x with
| ⟨S, property⟩ => S.sum idkey:2 ^ A.card ≤ A.card * N + 1hc:A.card ≠ 0⊢ 1 ≤ ↑N All goals completed! 🐙]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 := ⊢ ∃ o,
∃ (_ : o =o[atTop] 1),
∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → (1 / 4 - o A.card) * 2 ^ A.card / √↑A.card ≤ ↑N
All goals completed! 🐙A number of improvements of the constant $\frac{1}{4}$ have been given, with the current record $\sqrt{2 / \pi}$ first provided in unpublished work of Elkies and Gleason.
@[category research solved, AMS 5 11,
formal_proof using formal_conjectures at
"https://github.com/MyTH-zyxeon/formal-conjectures/blob/362eed1a8864d142ae65f51af7981a7c7530956e/FormalConjectures/Scratch/HarperCompression.lean#L2174"]
theorem erdos_1.variants.lb_strong : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N),
(√(2 / π) - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N := ⊢ ∃ o,
∃ (_ : o =o[atTop] 1),
∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → (√(2 / π) - o A.card) * 2 ^ A.card / √↑A.card ≤ ↑N
All goals completed! 🐙A finite set of real numbers is said to be sum-distinct if all the subset sums differ by at least $1$.
abbrev IsSumDistinctRealSet (A : Finset ℝ) (N : ℕ) : Prop :=
↑A ⊆ Set.Ioc (0 : ℝ) N ∧ (A.powerset : Set (Finset ℝ)).Pairwise fun S₁ S₂ =>
1 ≤ dist (S₁.sum id) (S₂.sum id)A generalisation of the problem to sets $A \subseteq (0, N]$ of real numbers, such that the subset sums all differ by at least $1$ is proposed in [Er73] and [ErGr80].
The positive statement is false: every natural-number counterexample to erdos_1 embeds into
$\mathbb{R}$, and distinct integer subset sums differ by at least one.
[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).