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 Filter open scoped Topology Real namespace 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 declaration uses 'sorry'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$.

@[category textbook, AMS 5 11] theorem erdos_1.variants.weaker : ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ) (_ : IsSumDistinctSet A N), N ≠ 0 → C * 2 ^ A.card / A.card < N := ⊢ ∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card / ↑A.card < ↑N refine ⟨1/3, ⊢ 1 / 3 > 0 All goals completed! 🐙, fun N A ⟨hA1, hA2⟩ hN => ?_⟩ have key : 2 ^ A.card ≤ A.card * N + 1 := ⊢ ∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card / ↑A.card < ↑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 id⊢ A.powerset.card ≤ A.card * N + 1 exact (Finset.card_le_card_of_injOn (Finset.sum · id) (fun S hS => Finset.mem_range.mpr <| Nat.lt_add_one_of_le <| (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).2).trans (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))) (fun a ha b hb hab => 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 ida:Finset ℕha:a ∈ ↑A.powersetb:Finset ℕhb:b ∈ ↑A.powersethab:(fun x => x.sum id) a = (fun x => x.sum id) b⊢ a = b 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 ida:Finset ℕha:a ∈ ↑A.powersetb:Finset ℕhb:b ∈ ↑A.powersethab:(fun x => x.sum id) a = (fun x => x.sum id) bthis:⟨a, ha⟩ = ⟨b, hb⟩ := hA2 hab⊢ a = b; 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 ida:Finset ℕha:a ∈ ↑A.powersetb:Finset ℕhb:b ∈ ↑A.powersethab:(fun x => x.sum id) a = (fun x => x.sum id) bthis:a = b⊢ a = b; All goals completed! 🐙)).trans_eq (Finset.card_range _) 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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc:A.card = 0⊢ 1 / 3 * 2 ^ A.card / ↑A.card < ↑NN:ℕ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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc:A.card ≠ 0⊢ 1 / 3 * 2 ^ A.card / ↑A.card < ↑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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc:A.card = 0⊢ 1 / 3 * 2 ^ A.card / ↑A.card < ↑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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc:A.card = 0⊢ 0 < N; All goals completed! 🐙 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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc:A.card ≠ 0⊢ 1 / 3 * 2 ^ A.card / ↑A.card < ↑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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc: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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc: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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc: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 + 1 := Eq.mpr (id (congrArg (fun _a => _a ≤ A.card * N + 1) (Eq.symm (Finset.card_powerset A)))) (LE.le.trans_eq (Finset.card_le_card_of_injOn (fun x => x.sum id) (fun S hS => Finset.mem_range.mpr (Nat.lt_add_one_of_le (LE.le.trans (Finset.sum_le_card_nsmul S id N fun i hi => (Finset.mem_Icc.mp (hA1 (Finset.mem_powerset.mp hS hi))).right) (Nat.mul_le_mul_right N (Finset.card_le_card (Finset.mem_powerset.mp hS)))))) fun a ha b hb hab => have this := hA2 hab; Eq.mp (Subtype.mk.injEq a ha b hb) this) (Finset.card_range (A.card * N + 1)))hc: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 declaration uses 'sorry'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 provied in unpublished work of Elkies and Gleason.

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'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 declaration uses 'sorry'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

@[category textbook, AMS 5 11] theorem erdos_1.variants.least_N_3 : IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4 := ⊢ IsLeast {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3} 4 ⊢ IsSumDistinctSet {1, 2, 4} 4 ∧ {1, 2, 4}.card = 3⊢ 4 ∈ lowerBounds {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3} ⊢ IsSumDistinctSet {1, 2, 4} 4 ∧ {1, 2, 4}.card = 3 ⊢ IsSumDistinctSet {1, 2, 4} 4 refine ⟨⊢ {1, 2, 4} ⊆ Finset.Icc 1 4 All goals completed! 🐙, ?_⟩ P:Finset (Finset ℕ) := {1, 2, 4}.powerset⊢ Function.Injective fun x => match x with | ⟨S, property⟩ => S.sum id have : Finset.univ.image (fun p : P ↦ ∑ x ∈ p, x) = {0, 1, 2, 4, 3, 5, 6, 7} := ⊢ IsLeast {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3} 4 P:Finset (Finset ℕ) := {1, 2, 4}.powersetn:ℕ⊢ n ∈ Finset.image (fun p => ∑ x ∈ ↑p, x) Finset.univ ↔ n ∈ {0, 1, 2, 4, 3, 5, 6, 7} P:Finset (Finset ℕ) := {1, 2, 4}.powersetn:ℕ⊢ 0 = n ∨ 1 = n ∨ 2 = n ∨ 4 = n ∨ 3 = n ∨ 5 = n ∨ 6 = n ∨ 7 = n ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ n = 3 ∨ n = 5 ∨ n = 6 ∨ n = 7 All goals completed! 🐙 P:Finset (Finset ℕ) := {1, 2, 4}.powersetthis:Finset.image (fun p => ∑ x ∈ ↑p, x) Finset.univ = {0, 1, 2, 4, 3, 5, 6, 7} := Finset.ext_iff.mpr fun n => Eq.mpr (id (congr (congrArg Iff (Eq.trans Finset.mem_image._simp_1 (Eq.trans (Eq.trans (congrArg Exists (funext fun a => Eq.trans (congrArg (fun x => x ∧ ∑ x ∈ ↑a, x = n) (Finset.mem_attach._simp_1 P a)) (true_and (∑ x ∈ ↑a, x = n)))) Subtype.exists._simp_1) (Eq.trans (Eq.trans (congrArg Exists (funext fun a => Eq.trans (propext (exists_prop_congr (fun h => Iff.of_eq (Eq.refl (∑ x ∈ a, x = n))) (Iff.of_eq (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (have this := of_decide_eq_true (id (Eq.refl true)); this)) Finset.mem_insert._simp_1) (congrArg (Or (a = ∅)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {2})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {4})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1, 2})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1, 4})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {2, 4})) Finset.mem_singleton._simp_1))))))))))))))))) exists_prop._simp_1)) exists_eq_or_imp._simp_1) (congrArg (Or (0 = n)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 1)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 2)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 4)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Finset.sum_singleton (fun x => x) 2)))) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 4))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Finset.sum_singleton (fun x => x) 4)))) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false_of_decide (Eq.refl false)))) not_false_eq_true))) (congrArg (HAdd.hAdd 2) (Finset.sum_singleton (fun x => x) 4)))) (Eq.trans (propext { mp := fun a => Exists.elim a fun a a_1 => ⟨rfl, Eq.mp (congrArg (fun a => ∑ x ∈ a, x = n) a_1.left) a_1.right⟩, mpr := fun a => Exists.intro {1, 2, 4} ⟨rfl, a.right⟩ }) (Eq.trans (congr (congrArg And (eq_self {1, 2, 4})) (congrArg (fun x => x = n) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (OfNat.one_ne_ofNat._simp_1 2)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 4))) (or_self False)))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false_of_decide (Eq.refl false)))) not_false_eq_true))) (congrArg (HAdd.hAdd 2) (Finset.sum_singleton (fun x => x) 4))))))) (true_and (7 = n))))))))))))))))))))) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 0)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 1)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 2)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 4)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 3)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 5)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 6)) Finset.mem_singleton._simp_1)))))))))))))))) (Decidable.byContradiction fun a => least_N_3._proof_1 n a)⊢ Set.InjOn (fun x => match x with | ⟨S, property⟩ => S.sum id) ↑Finset.univ have : (Finset.univ.image (fun p : P ↦ ∑ x ∈ p.1, x)).card = (Finset.univ (α := P)).card := ⊢ IsLeast {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3} 4 P:Finset (Finset ℕ) := {1, 2, 4}.powersetthis:Finset.image (fun p => ∑ x ∈ ↑p, x) Finset.univ = {0, 1, 2, 4, 3, 5, 6, 7} := Finset.ext_iff.mpr fun n => Eq.mpr (id (congr (congrArg Iff (Eq.trans Finset.mem_image._simp_1 (Eq.trans (Eq.trans (congrArg Exists (funext fun a => Eq.trans (congrArg (fun x => x ∧ ∑ x ∈ ↑a, x = n) (Finset.mem_attach._simp_1 P a)) (true_and (∑ x ∈ ↑a, x = n)))) Subtype.exists._simp_1) (Eq.trans (Eq.trans (congrArg Exists (funext fun a => Eq.trans (propext (exists_prop_congr (fun h => Iff.of_eq (Eq.refl (∑ x ∈ a, x = n))) (Iff.of_eq (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (have this := of_decide_eq_true (id (Eq.refl true)); this)) Finset.mem_insert._simp_1) (congrArg (Or (a = ∅)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {2})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {4})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1, 2})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {1, 4})) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (a = {2, 4})) Finset.mem_singleton._simp_1))))))))))))))))) exists_prop._simp_1)) exists_eq_or_imp._simp_1) (congrArg (Or (0 = n)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 1)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 2)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Finset.sum_singleton (fun x => x) 4)) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Finset.sum_singleton (fun x => x) 2)))) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 4))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Finset.sum_singleton (fun x => x) 4)))) (Eq.trans exists_eq_or_imp._simp_1 (congr (congrArg (fun x => Or (x = n)) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false_of_decide (Eq.refl false)))) not_false_eq_true))) (congrArg (HAdd.hAdd 2) (Finset.sum_singleton (fun x => x) 4)))) (Eq.trans (propext { mp := fun a => Exists.elim a fun a a_1 => ⟨rfl, Eq.mp (congrArg (fun a => ∑ x ∈ a, x = n) a_1.left) a_1.right⟩, mpr := fun a => Exists.intro {1, 2, 4} ⟨rfl, a.right⟩ }) (Eq.trans (congr (congrArg And (eq_self {1, 2, 4})) (congrArg (fun x => x = n) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (OfNat.one_ne_ofNat._simp_1 2)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 4))) (or_self False)))) not_false_eq_true))) (congrArg (HAdd.hAdd 1) (Eq.trans (Finset.sum_insert (of_eq_true (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false_of_decide (Eq.refl false)))) not_false_eq_true))) (congrArg (HAdd.hAdd 2) (Finset.sum_singleton (fun x => x) 4))))))) (true_and (7 = n))))))))))))))))))))) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 0)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 1)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 2)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 4)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 3)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 5)) (Eq.trans Finset.mem_insert._simp_1 (congrArg (Or (n = 6)) Finset.mem_singleton._simp_1)))))))))))))))) (Decidable.byContradiction fun a => least_N_3._proof_1 n a)⊢ {0, 1, 2, 4, 3, 5, 6, 7}.card = Finset.univ.card; All goals completed! 🐙 All goals completed! 🐙 ⊢ 4 ∈ lowerBounds {N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3} ⊢ ∀ (x : ℕ), ∀ x_1 ⊆ Finset.Icc 1 x, (Function.Injective fun x => ∑ x ∈ ↑x, x) → x_1.card = 3 → 4 ≤ x intro n n:ℕS:Finset ℕ⊢ S ⊆ Finset.Icc 1 n → (Function.Injective fun x => ∑ x ∈ ↑x, x) → S.card = 3 → 4 ≤ n n:ℕS:Finset ℕh:S ⊆ Finset.Icc 1 n⊢ (Function.Injective fun x => ∑ x ∈ ↑x, x) → S.card = 3 → 4 ≤ n n:ℕS:Finset ℕh:S ⊆ Finset.Icc 1 nh_inj:Function.Injective fun x => ∑ x ∈ ↑x, x⊢ S.card = 3 → 4 ≤ n n:ℕS:Finset ℕh:S ⊆ Finset.Icc 1 nh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3⊢ 4 ≤ n n:ℕS:Finset ℕh:S ⊆ Finset.Icc 1 nh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3hn:¬4 ≤ n⊢ False n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 0hn:¬4 ≤ 0⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 1hn:¬4 ≤ 1⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 2hn:¬4 ≤ 2⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 3hn:¬4 ≤ 3⊢ False; n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 1hn:¬4 ≤ 1⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 2hn:¬4 ≤ 2⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 3hn:¬4 ≤ 3⊢ False; n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 2hn:¬4 ≤ 2⊢ Falsen:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 3hn:¬4 ≤ 3⊢ False n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 2hn:¬4 ≤ 2⊢ False n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 2hn:¬4 ≤ 2this:S.card ≤ (Finset.Icc 1 2).card := Finset.card_le_card h⊢ False All goals completed! 🐙 n:ℕS:Finset ℕh_inj:Function.Injective fun x => ∑ x ∈ ↑x, xhcard3:S.card = 3h:S ⊆ Finset.Icc 1 3hn:¬4 ≤ 3⊢ False 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 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 declaration uses 'sorry'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 declaration uses 'sorry'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