Erdos 43 #307

Krishn1412 · 2025-07-04T12:38:55Z

Proposed formal conjecture for Erdos problem 43.

google-cla · 2025-07-04T12:38:59Z

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

…conjectures into erdos_prob_43

mo271

Thanks for the contribution!

FormalConjectures/ErdosProblems/43.lean

callesonne

Thanks for your contribution! Here are some comments :)

FormalConjectures/ErdosProblems/43.lean

FormalConjectures/ForMathlib/Combinatorics/Basic.lean

FormalConjectures/ErdosProblems/43.lean

Krishn1412 · 2025-07-25T18:50:56Z

Hey @mo271, could you help me out on why this is failing? Any pointers would be great, TIA!

Paul-Lez

One minor comment - I'll try to diagnose the build issue once I'm back in front of a computer:)

FormalConjectures/ForMathlib/Combinatorics/Basic.lean

mo271 · 2025-07-26T13:03:51Z

Hey @mo271, could you help me out on why this is failing? Any pointers would be great, TIA!

seems like there were some problems in ForMathlib/Combinatorics/Basic.lean, starting with a failing import.
Should be something like this:

import FormalConjectures.ForMathlib.Combinatorics.AP.Basic
import Mathlib.Combinatorics.Enumerative.Bell
import Mathlib.Combinatorics.SimpleGraph.Finite

open Function Set

variable {α : Type*} [AddCommMonoid α]

/-- A Sidon set is a set such that all pairwise sums of elements are distinct,
apart from coincidences forced by commutativity. -/
def IsSidon (A : Set α) : Prop := ∀ᵉ (i₁ ∈ A) (j₁ ∈ A) (i₂ ∈ A) (j₂ ∈ A),
  i₁ + i₂ = j₁ + j₂ → (i₁ = j₁ ∧ i₂ = j₂) ∨ (i₁ = j₂ ∧ i₂ = j₁)

lemma IsSidon.avoids_isAPOfLength_three {α : Type*} [AddCommMonoid α] (A : Set ℕ) (hA : IsSidon A) :
    (∀ Y, IsAPOfLength Y 3 → (A ∩ Y).ncard ≤ 2) := by
  sorry

noncomputable instance IsSidon.decide [AddCommMonoid α] (s : Set α): Decidable (IsSidon s) := by
  exact Classical.propDecidable _

/-- The subsets of `{0, ..., n - 1}` which are Sidon sets. -/
noncomputable def SidonSubsets (n : ℕ) : Finset (Finset ℕ) :=
  (Finset.range n).powerset.filter fun s => IsSidon (s : Set ℕ)

/-- The sizes of Sidon subsets of `{0, ..., n - 1}`. -/
noncomputable def SidonSubsetsSizes (n : ℕ) : Finset ℕ :=
  (SidonSubsets n).image Finset.card

lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by
  use 0
  simp only [SidonSubsetsSizes, Finset.mem_image]
  use ∅
  simp [SidonSubsets, IsSidon, Set.Pairwise, Finset.mem_filter, Finset.mem_powerset, Finset.card_empty]

/-- The maximum size of a Sidon subset of `{0, ..., n - 1}`. -/
noncomputable def maxSidonSetSize (n : ℕ) : ℕ :=
  (SidonSubsetsSizes n).max' (SidonSubsetsSizesNonempty n)

mo271 · 2025-07-27T13:06:10Z

@Krishn1412 Thanks for reacting to the comments and updating the pr! It would make the review easier if you resolved the comments that are already addressed.

Krishn1412 · 2025-07-27T13:41:50Z

Sure @mo271

mo271 · 2025-09-05T13:26:54Z

@Krishn1412 in the meantime some definitions around Sidon have changed. Would you be able to integrate the pull request into the new FormalConjectures/ForMathlib/Combinatorics/Basic.lean or shall I?

Krishn1412 · 2025-09-06T17:07:48Z

Sure, I will update the PR. I was wondering if you found the issue causing the build failure.

mo271 · 2025-09-07T08:53:22Z

FormalConjectures/ForMathlib/Combinatorics/Basic.lean

+noncomputable def SidonSubsetsSizes (n : ℕ) : Finset ℕ :=
+  (SidonSubsets n).image Finset.card
+
+lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by


Suggested change

lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by

lemma SidonSubsetsSizes_nonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by

I think since this is a lemma we would use small caps here?

mo271 · 2025-09-07T08:55:39Z

FormalConjectures/ErdosProblems/43.lean

+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      (A - A) ∩ (B - B) = ∅ →


Suggested change

(A - A) ∩ (B - B) = ∅ →

(A - A) ∩ (B - B) = {0} →

In both A - A and B-B, there will always be 0, if both sets are nonempty.

mo271 · 2025-09-07T09:00:29Z

FormalConjectures/ErdosProblems/43.lean

+If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,
+is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?


Suggested change

If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,

is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?

If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets such that $(A-A)\cap(B-B)=\{0\}$

then is it true that

$$\binom{\lvert A\rvert}{2}+\binom{\lvert B\rvert}{2}\leq\binom{f(N)}{2}+O(1),$$

where $f(N)$ is the maximum possible size of a Sidon set in \{1,\ldots,N\}?

Better to stick to the original formulation.

mo271 · 2025-09-07T09:01:39Z

FormalConjectures/ErdosProblems/43.lean

+is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43 :


since this is phrased as a questions, we should wrap the entire statement in parenthesis and write ↔ answer(sorry)

mo271 · 2025-09-07T09:02:24Z

FormalConjectures/ErdosProblems/43.lean

+If `A` and `B` are equal-sized Sidon sets with disjoint difference sets,
+can the sum of pair counts be bounded by a strict fraction of the optimum?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43_equal_size :
+    ∃ᵉ (c > 0), ∀ (N : ℕ) (A B : Finset ℕ),
+      A ⊆ Finset.Icc 1 N →
+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      A.card = B.card →
+      (A - A) ∩ (B - B) = ∅ →
+      A.card.choose 2 + B.card.choose 2 ≤ (1 - c) *(maxSidonSetSize N).choose 2 := by
+  sorry


same comments as to the first theorem apply here.

mo271 · 2025-09-07T09:03:12Z

Sure, I will update the PR. I was wondering if you found the issue causing the build failure.

@Krishn1412 I updated the PR and fixed the issue causing the build failure.

Erdos 43

4c87eae

Proposed formal conjecture for Erdos problem 43.

Krishn1412 added 3 commits July 4, 2025 18:10

Merge branch 'main' into erdos_prob_43

42ef9ec

Fixing missing identifier issues

fdd33e8

Merge branch 'erdos_prob_43' of https://github.com/Krishn1412/formal-…

8c0e1a5

…conjectures into erdos_prob_43

mo271 approved these changes Jul 6, 2025

View reviewed changes

FormalConjectures/ErdosProblems/43.lean Outdated Show resolved Hide resolved

FormalConjectures/ErdosProblems/43.lean Outdated Show resolved Hide resolved

FormalConjectures/ErdosProblems/43.lean Show resolved Hide resolved

Updates based on comments

2d87566

callesonne reviewed Jul 11, 2025

View reviewed changes

Krishn1412 added 2 commits July 19, 2025 12:15

updates based on review

4ed0afb

Merge branch 'main' into erdos_prob_43

35b40cf

Paul-Lez reviewed Jul 26, 2025

View reviewed changes

FormalConjectures/ForMathlib/Combinatorics/Basic.lean Outdated Show resolved Hide resolved

Updates

747be5f

mo271 added the Erdős Problems label Aug 19, 2025

Merge branch 'main' into erdos_prob_43

c6e7ecc

mo271 added the Awaiting author A reviewer has asked the author a question or requested changes. label Aug 19, 2025

mo271 added 4 commits September 7, 2025 10:38

Merge branch 'main' into erdos_prob_43

815e023

fix build

751efab

min imports

ed2cf46

min imports

a6e0082

mo271 reviewed Sep 7, 2025

View reviewed changes

	lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by
	lemma SidonSubsetsSizes_nonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by

		If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,
		is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?

-If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,
-is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?
+If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets such that $(A-A)\cap(B-B)=\{0\}$
+then is it true that
+$$\binom{\lvert A\rvert}{2}+\binom{\lvert B\rvert}{2}\leq\binom{f(N)}{2}+O(1),$$
+where $f(N)$ is the maximum possible size of a Sidon set in \{1,\ldots,N\}?

Uh oh!

Erdos 43 #307

Are you sure you want to change the base?

Erdos 43 #307

Uh oh!

Conversation

Krishn1412 commented Jul 4, 2025

Uh oh!

google-cla bot commented Jul 4, 2025

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

callesonne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Krishn1412 commented Jul 25, 2025

Uh oh!

Paul-Lez left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mo271 commented Jul 26, 2025

Uh oh!

mo271 commented Jul 27, 2025

Uh oh!

Krishn1412 commented Jul 27, 2025

Uh oh!

mo271 commented Sep 5, 2025

Uh oh!

Krishn1412 commented Sep 6, 2025

Uh oh!

mo271 Sep 7, 2025

Choose a reason for hiding this comment

Uh oh!

mo271 Sep 7, 2025

Choose a reason for hiding this comment

Uh oh!

mo271 Sep 7, 2025

Choose a reason for hiding this comment

Uh oh!

mo271 Sep 7, 2025

Choose a reason for hiding this comment

Uh oh!

mo271 Sep 7, 2025

Choose a reason for hiding this comment

Uh oh!

mo271 commented Sep 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mo271 commented Sep 7, 2025 •

edited

Loading