1. FormalConjectures
  2. ErdosProblems
  3. «1»
/- 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. -/ import FormalConjecturesUtil

Erdős Problem 1

Reference: erdosproblems.com/1

open Filteropen scoped Topology Realnamespace Erdos1

A 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).Injective

If $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. $$

@[category research open, AMS 5 11] 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] 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].

[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).

@[category research open, AMS 5 11] theorem erdos_1.variants.real : ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℝ) (_ : IsSumDistinctRealSet A N), N ≠ 0 → C * 2 ^ A.card < N := ⊢ ∃ C > 0, ∀ (N : ℕ) (A : Finset ℝ), IsSumDistinctRealSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N All goals completed! 🐙

The minimal value of $N$ such that there exists a sum-distinct set with three elements is $4$.

https://oeis.org/A276661

n:ℕS:Finset ℕh_inj:Function.Injective fun x ↦ ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 3hn:¬4 ≤ 3⊢ ¬Function.Injective fun x ↦ ∑ x ∈ ↑x, x All goals completed! 🐙

The minimal value of $N$ such that there exists a sum-distinct set with five elements is $13$.

https://oeis.org/A276661

@[category research solved, AMS 5 11] theorem erdos_1.variants.least_N_5 : IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 5 } 13 := ⊢ IsLeast {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 5} 13 All goals completed! 🐙

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 := ⊢ IsLeast {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 9} 161 All goals completed! 🐙end Erdos1