Erdős Problem 44: Extending… to Erdős Problem 66

TheoremErdős Problem 44: Extending Sidon Sets#

References: - erdosproblems.com/44 - [Si38] Singer, James, A theorem in finite projective geometry and some applications to number theory. Trans. Amer. Math. Soc. (1938), 377--385.

Quoted from FormalConjectures/ErdosProblems/44.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/44.

The file states 6 research or textbook statements: 1 open, 1 solved and 4 textbook results.

Erdos44.maxSidonSubsetCard_icc_bound

Textbook result, proved here.

The maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.

theorem maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) :
    maxSidonSubsetCard (Icc 1 N) ≤ 2 * Real.sqrt N

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 38.

Erdos44.erdos_44

Open: stated without proof.

Erdős Problem 44: Let N ≥ 1 and A ⊆ {1,…,N} be a Sidon set. Is it true that, for any ε > 0, there exist M = M(ε) and B ⊆ {N+1,…,M} such that A ∪ B ⊆ {1,…,M} is a Sidon set of size at least (1−ε)M^{1/2}?

This problem asks whether any Sidon set can be extended to achieve a density arbitrarily close to the optimal density for Sidon sets.

theorem erdos_44 : ∀ᵉ (N ≥ (1 : ℕ)) (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) →
    ∀ᵉ (ε > (0 : ℝ)), ∃ᵉ (M > N) (B ⊆ Finset.Icc (N + 1) M),
      IsSidon (A ∪ B : Set ℕ) ∧ (1 - ε) * Real.sqrt M ≤ (A ∪ B).card

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 92.

Erdos44.erdos_44.variants.empty_start

Solved: stated here without proof.

The case where we start with an empty set (constructing large Sidon sets).

The answer is yes. Singer [Si38] constructed Sidon sets of size \(q + 1\) in \(\{1, \ldots, q^2 + q + 1\}\) for every prime \(q\). Since \(p_{n+1}/p_n \to 1\) for consecutive primes, this gives Sidon sets of size \((1 - o(1))M^{1/2}\) in \(\{1, \ldots, M\}\) for every \(M\); see erdosproblems.com/30.

theorem erdos_44.variants.empty_start : ∀ᵉ (ε > (0 : ℝ)), ∀ᶠ (M : ℕ) in Filter.atTop,
    ∃ᵉ (A ⊆ Finset.Icc 1 M), IsSidon (A : Set ℕ) ∧ (1 - ε) * Real.sqrt M ≤ A.card

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 106.

Erdos44.example_sidon_set

Textbook result, proved here.

The set {1, 2, 4, 8, 13} is a Sidon set in {1, ..., 13}.

theorem example_sidon_set : IsSidon ({1, 2, 4, 8, 13} : Set ℕ)

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 116.

Erdos44.sidon_set_lower_bound

Textbook result, stated without proof.

For any N, there exists a Sidon set of size at least √N/2.

theorem sidon_set_lower_bound (N : ℕ) (hN : 1 ≤ N) :
    ∃ᵉ (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) ∧ Real.sqrt N / 2 ≤ A.card

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 129.

Erdos44.greedy_sidon_construction

Textbook result, stated without proof.

The greedy construction gives a Sidon set A ⊆ {1, ..., N} of size at least \(N^{1/3}\), stated here as \(N \le |A|^3\). See Section 1 of arXiv:2103.15850.

theorem greedy_sidon_construction (N : ℕ) (hN : 1 ≤ N) :
    ∃ᵉ (A ⊆ Finset.Icc 1 N), IsSidon (A : Set ℕ) ∧ N ≤ A.card ^ 3

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/44.lean, line 138.

Sources

• FormalConjectures/ErdosProblems/44.lean at 2055e5ad
• erdosproblems.com/44

LeanErdos44.maxSidonSubsetCard_icc_bound · Erdos44.erdos_44 · Erdos44.erdos_44.variants.empty_start · Erdos44.example_sidon_set · Erdos44.sidon_set_lower_bound · Erdos44.greedy_sidon_construction

TheoremErdős Problem 45#

References: - erdosproblems.com/45 - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333-335. - [Cr03] Croot, III, Ernest S., On a coloring conjecture about unit fractions. Ann. of Math. (2) (2003), 545-556. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.

Quoted from FormalConjectures/ErdosProblems/45.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/45.

The file states 1 research or textbook statement: 1 solved.

Erdos45.erdos_45

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos45.lean.

Let \(k\geq 2\). Is there an integer \(n_k\) such that, if \(D=\{ 1\lt d\lt n_k : d\mid n_k\}\), then for any \(k\)-colouring of \(D\) there is a monochromatic subset \(D'\subseteq D\) such that \(\sum_{d\in D'}\frac{1}{d}=1\)?

This follows from the colouring result of Croot [Cr03]. Croot's result allows for \(n_k \leq e^{C^k}\) for some constant \(C>1\) (simply taking \(n_k\) to be the lowest common multiple of some interval \([1,C^k]\)). Sawhney has observed that there is also a doubly exponential lower bound, and hence this bound is essentially sharp.

theorem erdos_45 :
    ∀ k : ℕ, 2 ≤ k → ∃ n : ℕ, ∀ colouring : ℕ → Fin k,
      ∃ colour : Fin k, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n},
        (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/45.lean, line 50.

Sources

• FormalConjectures/ErdosProblems/45.lean at 2055e5ad
• erdosproblems.com/45

LeanErdos45.erdos_45

TheoremErdős Problem 46#

References: - erdosproblems.com/46 - [Cr03] Croot, III, Ernest S., On a coloring conjecture about unit fractions. Ann. of Math. (2) (2003), 545-556. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

Quoted from FormalConjectures/ErdosProblems/46.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/46.

The file states 3 research or textbook statements: 3 solved.

Erdos46.erdos_46

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos46.lean.

Does every finite colouring of the integers have a monochromatic solution to \(1=\sum \frac{1}{n_i}\) with \(2\leq n_1\lt \cdots \lt n_k\)?

The answer is yes, as proved by Croot [Cr03] - indeed, there are infinitely many disjoint such monochromatic solutions.

theorem erdos_46 :
    -- For any finite colouring of the integers
    ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite →
      -- there are integers `2 ≤ n₁ < ⋯ < n_k`
      ∃ S : Finset ℕ, (∀ n ∈ S, 2 ≤ n) ∧
        -- whose reciprocals sum to `1`
        ∑ n ∈ S, (1 / n : ℚ) = 1 ∧
        -- and which all have the same colour
        (𝓒 '' (S : Set ℕ)).Subsingleton

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/46.lean, line 44.

Erdos46.erdos_46.variants.infinitely_many_disjoint

Solved: stated here without proof.

Croot [Cr03] proved more: there are infinitely many disjoint such monochromatic solutions.

theorem erdos_46.variants.infinitely_many_disjoint :
    ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite →
      ∃ S : ℕ → Finset ℕ, (∀ i j, i ≠ j → Disjoint (S i) (S j)) ∧
        ∀ i, (∀ n ∈ S i, 2 ≤ n) ∧ ∑ n ∈ S i, (1 / n : ℚ) = 1 ∧
          (𝓒 '' (S i : Set ℕ)).Subsingleton

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/46.lean, line 59.

Erdos46.erdos_46.variants.positive_rat

Solved: stated here without proof.

In [ErGr80] they also ask for a monochromatic representation of any \(\frac{a}{b}>0\).

theorem erdos_46.variants.positive_rat :
    ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∀ q : ℚ, 0 < q →
      ∃ S : Finset ℕ, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, (1 / n : ℚ) = q ∧
        (𝓒 '' (S : Set ℕ)).Subsingleton

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/46.lean, line 70.

Sources

• FormalConjectures/ErdosProblems/46.lean at 2055e5ad
• erdosproblems.com/46

LeanErdos46.erdos_46 · Erdos46.erdos_46.variants.infinitely_many_disjoint · Erdos46.erdos_46.variants.positive_rat

TheoremErdős Problem 47#

References: - erdosproblems.com/47 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34-50. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333-335. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021). - [LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024).

Quoted from FormalConjectures/ErdosProblems/47.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/47.

The file states 1 research or textbook statement: 1 solved.

Erdos47.erdos_47

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos47.lean.

If \(\delta>0\) and \(N\) is sufficiently large in terms of \(\delta\), and \(A\subseteq\{1,\ldots,N\}\) is such that \(\sum_{a\in A}\frac{1}{a}>\delta \log N\) then must there exist \(S\subseteq A\) such that \(\sum_{n\in S}\frac{1}{n}=1\)?

Bloom [Bl21] proved this in the affirmative.

theorem erdos_47 :
    ∀ δ : ℝ, 0 < δ → ∀ᶠ N : ℕ in atTop, ∀ A : Finset ℕ,
      A ⊆ Finset.Icc 1 N →
      δ * Real.log (N : ℝ) < A.reciprocalSum →
      ∃ S : Finset ℕ, S ⊆ A ∧ S.reciprocalSum = 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/47.lean, line 58.

Sources

• FormalConjectures/ErdosProblems/47.lean at 2055e5ad
• erdosproblems.com/47

LeanErdos47.erdos_47

TheoremErdős Problem 48#

Reference: erdosproblems.com/48

Quoted from FormalConjectures/ErdosProblems/48.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/48.

The file states 1 research or textbook statement: 1 solved.

Erdos48.erdos_48

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos48.lean#L599.

Are there infinitely many integers \(n, m\) such that \(ϕ(n) = σ(m)\)?

theorem erdos_48 :
    {(n, m) : ℕ × ℕ | n.totient = σ 1 m}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/48.lean, line 38.

Sources

• FormalConjectures/ErdosProblems/48.lean at 2055e5ad
• erdosproblems.com/48

LeanErdos48.erdos_48

TheoremErdős Problem 49#

References: - erdosproblems.com/49 - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er95c] Erdős, Paul, Some problems in number theory. Octogon Math. Mag. (1995), 3-5. - [Ta24d] Tao, Terence, Monotone nondecreasing sequences of the Euler totient function. Matematica (2024), 793-820.

Quoted from FormalConjectures/ErdosProblems/49.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/49.

The file states 4 research or textbook statements: 1 open and 3 solved.

Erdos49.erdos_49

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos49.lean#L120.

Let \(A=\{a_1\lt \cdots\lt a_t\}\subseteq \{1,\ldots,N\}\) be such that \(\phi(a_1)\lt \cdots\lt \phi(a_t)\). The primes are such an example. Are they the largest possible? Can one show that \(\lvert A\rvert<(1+o(1))\pi(N)\) or even \(\lvert A\rvert=o(N)\)?

Erdős remarks that the last conjecture is probably easy, and that similar questions can be asked about \(\sigma(n)\).

Solved by Tao [Ta24d], who proved that

\[ \lvert A\rvert \leq \left(1+O\left(\frac{(\log\log x)^5}{\log x}\right)\right)\pi(x).\]

In [Er95c] Erdős further asks about the situation when \(\phi(a_1)\leq \cdots \leq \phi(a_t)\).

See also 415.

theorem erdos_49 : ∀ ε : ℝ, 0 < ε →
    ∀ᶠ N : ℕ in atTop, (f N : ℝ) ≤ (1 + ε) * Nat.primeCounting N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/49.lean, line 68.

Erdos49.erdos_49.variants.little_o

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos49.lean#L340.

The weaker statement \(\lvert A\rvert=o(N)\).

theorem erdos_49.variants.little_o :
    (fun N : ℕ ↦ (f N : ℝ)) =o[atTop] fun N ↦ (N : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/49.lean, line 76.

Erdos49.erdos_49.variants.tao

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos49.lean#L120.

Tao [Ta24d] proved that \(\lvert A\rvert \leq \left(1+O\left(\frac{(\log\log N)^5}{\log N}\right)\right)\pi(N)\), even for sets on which \(\phi\) is merely non-decreasing.

theorem erdos_49.variants.tao : ∃ C : ℝ, 0 ≤ C ∧ ∀ N : ℕ, 10 ≤ N →
    (g N : ℝ) ≤ (1 + C * (Real.log (Real.log N) ^ 5 / Real.log N)) *
      Nat.primeCounting N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/49.lean, line 88.

Erdos49.erdos_49.variants.primes_maximal

Open: stated without proof.

Are the primes the largest possible example, i.e. is \(f(N) = \pi(N)\) for all \(N \geq 2\)?

theorem erdos_49.variants.primes_maximal :
    ∀ N : ℕ, 2 ≤ N → f N = Nat.primeCounting N

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/49.lean, line 95.

Sources

• FormalConjectures/ErdosProblems/49.lean at 2055e5ad
• erdosproblems.com/49

LeanErdos49.erdos_49 · Erdos49.erdos_49.variants.little_o · Erdos49.erdos_49.variants.tao · Erdos49.erdos_49.variants.primes_maximal

TheoremErdős Problem 50#

References: * erdosproblems.com/50 * [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. * [Sch38] Schoenberg, I. J. "On asymptotic distributions of arithmetical functions." Transactions of the American Mathematical Society 39.2 (1936): 315-330.

Quoted from FormalConjectures/ErdosProblems/50.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/50.

The file states 3 research or textbook statements: 1 open and 2 solved.

Erdos50.erdos_50_schoenberg

Solved: stated here without proof.

Schoenberg [Sch38] proved that the asymptotic distribution function of \(\varphi(n)/n\) exists. That is, for any \(c \in [0, 1]\), the proportion of integers \(n \le N\) satisfying \(\varphi(n)/n < c\) approaches a limit as \(N \to \infty\). This limit function is the cumulative distribution function of the values of \(\varphi(n)/n\).

theorem erdos_50_schoenberg : ∃ f : ℝ → ℝ, IsDistributionOfPhiRatio f

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/50.lean, line 61.

Erdos50.erdos_50_singular

Solved: stated here without proof.

Erdős [Er95] proved that the distribution function of \(\varphi(n)/n\) is purely singular on \([0, 1]\): it is continuous there, but its derivative is zero almost everywhere on \([0, 1]\).

theorem erdos_50_singular (f : ℝ → ℝ) (hf : IsDistributionOfPhiRatio f) :
    IsPurelySingularOn f (Icc 0 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/50.lean, line 69.

Erdos50.erdos_50

Open: stated without proof.

Let \(f\) be the asymptotic distribution function of \(\varphi(n)/n\), so that for each \(c \in [0,1]\), \(f(c)\) is the natural density of \(\{n : \varphi(n) < cn\}\). Is it true that there is no \(x\) such that the derivative \(f'(x)\) exists and is positive?

theorem erdos_50 : ∀ᵉ (f : ℝ → ℝ) (hf : IsDistributionOfPhiRatio f),
    ¬∃ x ∈ Icc (0 : ℝ) 1, ∃ y > 0, HasDerivWithinAt f y (Icc 0 1) x

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/50.lean, line 79.

Sources

• FormalConjectures/ErdosProblems/50.lean at 2055e5ad
• erdosproblems.com/50

LeanErdos50.erdos_50_schoenberg · Erdos50.erdos_50_singular · Erdos50.erdos_50

TheoremErdős Problem 51#

Reference: erdosproblems.com/51

Quoted from FormalConjectures/ErdosProblems/51.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/51.

The file states 1 research or textbook statement: 1 open.

Erdos51.erdos_51

Open: stated without proof.

Is there an infinite set \(A \subset \mathbb{N}\) such that for every \(a \in A\), there is an integer n such that \(\phi(n)=a\), and yet if \(n_a\) is the smallest such integer, then \(\frac{n_a}{a} → \infty\) as \(a → ∞\)?

theorem erdos_51 : ∃ A : Set ℕ, ∃ n : A → ℕ,
      A.Infinite ∧
      (∀ a : A, IsLeast (φ ⁻¹' {(a : ℕ)}) (n a)) ∧
      Tendsto (fun a : A => (n a : ℝ) / (a : ℝ)) atTop atTop

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/51.lean, line 39.

Sources

• FormalConjectures/ErdosProblems/51.lean at 2055e5ad
• erdosproblems.com/51

LeanErdos51.erdos_51

TheoremErdős Problem 52#

Reference: erdosproblems.com/52

Quoted from FormalConjectures/ErdosProblems/52.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/52.

The file states 1 research or textbook statement: 1 open.

Erdos52.erdos_52

Open: stated without proof.

Let \(A\) be a finite set of integers. Is it true that for every \(\epsilon>0\) \(\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A\rvert^{2-\epsilon}?\)

theorem erdos_52 : ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset ℤ),
    (max (A + A).card (A * A).card : ℝ) ≥ C * (A.card : ℝ) ^ (2 - ε)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/52.lean, line 37.

Sources

• FormalConjectures/ErdosProblems/52.lean at 2055e5ad
• erdosproblems.com/52

LeanErdos52.erdos_52

TheoremErdős Problem 53#

References: - erdosproblems.com/53 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErSz83] Erdős, P. and Szemerédi, E., On sums and products of integers. Studies in pure mathematics (1983), 213-218. - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [Er97] Erdős, Paul, Problems in number theory. New Zealand J. Math. (1997), 155-160. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Ch03] Chang, M.-C., The Erdős-Szemerédi problem on sum set and product set. Annals of Math. (2003), 939-957.

Quoted from FormalConjectures/ErdosProblems/53.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/53.

The file states 2 research or textbook statements: 2 solved.

Erdos53.erdos_53

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos53.lean#L3084.

Let \(A\) be a finite set of integers. Is it true that, for every \(k\), if \(\lvert A\rvert\) is sufficiently large depending on \(k\), then there are least \(\lvert A\rvert^k\) many integers which are either the sum or product of distinct elements of \(A\)?

Asked by Erdős and Szemerédi [ErSz83]. Solved in this form by Chang [Ch03].

Erdős and Szemerédi proved that there exist arbitrarily large sets \(A\) such that the number of integers which are the sum or product of distinct elements of \(A\) is at most

\[\exp\left(c \frac{(\log \lvert A\rvert)^2}{\log\log\lvert A\rvert}\right)\]

for some constant \(c>0\). (erdosproblems.com multiplies by \(\log\log\lvert A\rvert\); [ErSz83, Theorem 2] divides by it.)

See also 52.

theorem erdos_53 : ∀ k : ℕ, ∃ N : ℕ, ∀ A : Finset ℤ, N ≤ A.card →
    A.card ^ k ≤ (sumsAndProducts A).card

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/53.lean, line 68.

Erdos53.erdos_53.variants.upper

Solved: stated here without proof.

Erdős and Szemerédi [ErSz83] proved that there exist arbitrarily large sets \(A\) such that the number of integers which are the sum or product of distinct elements of \(A\) is at most

\[\exp\left(c \frac{(\log \lvert A\rvert)^2}{\log\log\lvert A\rvert}\right)\]

for some constant \(c>0\). (erdosproblems.com multiplies by \(\log\log\lvert A\rvert\); [ErSz83, Theorem 2] divides by it.)

theorem erdos_53.variants.upper : ∃ c : ℝ, 0 < c ∧ ∀ N : ℕ, ∃ A : Finset ℤ, N ≤ A.card ∧
    ((sumsAndProducts A).card : ℝ) ≤
      Real.exp (c * Real.log A.card ^ 2 / Real.log (Real.log A.card))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/53.lean, line 80.

Sources

• FormalConjectures/ErdosProblems/53.lean at 2055e5ad
• erdosproblems.com/53

LeanErdos53.erdos_53 · Erdos53.erdos_53.variants.upper

TheoremErdős Problem 56#

Reference: erdosproblems.com/56

Quoted from FormalConjectures/ErdosProblems/56.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/56.

The file states 1 research or textbook statement: 1 solved. It also has 5 test statements and 5 API statements, counted here but not shown.

Erdos56.erdos_56

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos56.lean.

Suppose \(A \subseteq \{1,\dots,N\}\) is such that there are no \(k+1\) elements of \(A\) which are relatively prime. An example is the set of all multiples of the first \(k\) primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that \(N\) be at least the \(k\)th prime.

theorem erdos_56 : ¬ ∀ᵉ (k > 0) (N ≥ (k-1).nth Nat.Prime),
    (MaxWeaklyDivisible N k = (FirstPrimesMultiples N k).card)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/56.lean, line 153.

Sources

• FormalConjectures/ErdosProblems/56.lean at 2055e5ad
• erdosproblems.com/56

LeanErdos56.erdos_56

TheoremErdős Problem 57#

References: - erdosproblems.com/57 - [ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99. - [LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).

Quoted from FormalConjectures/ErdosProblems/57.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/57.

The file states 1 research or textbook statement: 1 solved.

Erdos57.erdos_57

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos57.lean#L11124.

If \(G\) is a graph with infinite chromatic number and \(a_1 < a_2 < \cdots\) are lengths of the odd cycles of \(G\) then \(\sum \frac{1}{a_i} = \infty\).

Conjectured by Erdős and Hajnal [ErHa66], and solved by Liu and Montgomery [LiMo20].

The linked formal proof (Codex and GPT-5.6 Sol) states the conclusion as ¬ Summable (oddCycleReciprocal G), where oddCycleReciprocal G n is n⁻¹ if n is an odd cycle length of G and 0 otherwise; this is the indicator form of the sum below.

theorem erdos_57 :
    ∀ {V : Type*} (G : SimpleGraph V), G.chromaticNumber = ⊤ →
      ¬ Summable (fun (a : G.oddCycleLengths) ↦ 1 / (a : ℝ))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/57.lean, line 48.

Sources

• FormalConjectures/ErdosProblems/57.lean at 2055e5ad
• erdosproblems.com/57

LeanErdos57.erdos_57

TheoremErdős Problem 58#

References: - erdosproblems.com/58 - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [GaHuMa21] Gao, Jun and Huo, Qingyi and Ma, Jie, A strengthening on odd cycles in graphs of given chromatic number. SIAM J. Discrete Math. (2021), 2317-2327. - [Gy92] Gyárfás, A., Graphs with k odd cycle lengths. Discrete Math. (1992), 41-48.

Quoted from FormalConjectures/ErdosProblems/58.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/58.

The file states 1 research or textbook statement: 1 solved.

Erdos58.erdos_58

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/1f6f15be04f783cf5fabcf7f8477b4d8c03c685c/erdos-58/Proofs/Layer1358.lean#L35.

If \(G\) is a graph which contains odd cycles of \(\leq k\) different lengths then \(\chi(G)\leq 2k+2\), with equality if and only if \(G\) contains \(K_{2k+2}\).

Conjectured by Bollobás and Erdős. Proved by Gyárfás [Gy92].

theorem erdos_58 :
    ∀ {V : Type*} (G : SimpleGraph V) (k : ℕ),
      G.oddCycleLengths.Finite →
      G.oddCycleLengths.ncard ≤ k →
        G.chromaticNumber ≤ (2 * k + 2 : ℕ∞) ∧
        (G.chromaticNumber = (2 * k + 2 : ℕ∞) ↔
          (SimpleGraph.completeGraph (Fin (2 * k + 2))).IsContained G)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/58.lean, line 44.

Sources

• FormalConjectures/ErdosProblems/58.lean at 2055e5ad
• erdosproblems.com/58

LeanErdos58.erdos_58

TheoremErdős Problem 59#

References: - erdosproblems.com/59 - [EFR86] Erdős, P., Frankl, P. and Rödl, V., The asymptotic number of graphs not containing a fixed subgraph and a problem for hypergraphs having no exponent. Graphs Combin. (1986), 113-121. - [MoSa16] Morris, R. and Saxton, D., The number of \(C_{2\ell}\)-free graphs. Adv. Math. (2016), 534-580. arXiv:1309.2927 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

Quoted from FormalConjectures/ErdosProblems/59.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/59.

The file states 5 research or textbook statements: 2 open and 3 solved. It also has 1 API statement, counted here but not shown.

Erdos59.erdos_59

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos59.lean#L46.

Is it true that the number of graphs on \(n\) vertices which do not contain \(G\) is

\[\leq 2^{(1+o(1))\mathrm{ex}(n;G)}?\]

The answer is no, already for \(G=C_6\) (see erdos_59.variants.morris_saxton). Graphs are labelled, and \(G\) ranges over finite graphs containing a cycle, as in [MoSa16]; for some forests the answer is trivially no (for the path with two edges the free graphs include all matchings, about \(2^{\Theta(n\log n)}\) of them).

theorem erdos_59 :
    ¬ ∀ (k : ℕ) (H : SimpleGraph (Fin k)), ¬ H.IsAcyclic →
      ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
        (numFree H n : ℝ) ≤ (2 : ℝ) ^ ((1 + ε) * (extremalNumber n H : ℝ))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/59.lean, line 64.

Erdos59.erdos_59.variants.erdos_frankl_rodl

Solved: stated here without proof.

If \(G\) is not bipartite the answer is yes, proved by Erdős, Frankl, and Rödl [EFR86].

theorem erdos_59.variants.erdos_frankl_rodl {k : ℕ} (H : SimpleGraph (Fin k))
    (hH : ¬ H.IsBipartite) :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (numFree H n : ℝ) ≤ (2 : ℝ) ^ ((1 + ε) * (extremalNumber n H : ℝ))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/59.lean, line 74.

Erdos59.erdos_59.variants.morris_saxton

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos59.lean#L46.

The answer is no for \(G=C_6\), the cycle on 6 vertices. Morris and Saxton [MoSa16, Proposition 1.4] have proved there are at least

\[2^{(1+c)\mathrm{ex}(n;C_6)}\]

such graphs for infinitely many \(n\), for some constant \(c>0\).

theorem erdos_59.variants.morris_saxton :
    ∃ c : ℝ, 0 < c ∧ ∃ᶠ n : ℕ in atTop,
      (2 : ℝ) ^ ((1 + c) * (extremalNumber n (cycleGraph 6) : ℝ)) ≤
        (numFree (cycleGraph 6) n : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/59.lean, line 89.

Erdos59.erdos_59.variants.c4

Open: stated without proof.

In [Va99] the specific case of \(G=C_4\) is also asked.

theorem erdos_59.variants.c4 :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (numFree (cycleGraph 4) n : ℝ) ≤
        (2 : ℝ) ^ ((1 + ε) * (extremalNumber n (cycleGraph 4) : ℝ))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/59.lean, line 99.

Erdos59.erdos_59.variants.big_o

Open: stated without proof.

It is still possible (and conjectured by Morris and Saxton) that the weaker bound of

\[2^{O(\mathrm{ex}(n;G))}\]

holds for all \(G\) containing a cycle.

theorem erdos_59.variants.big_o :
    ∀ (k : ℕ) (H : SimpleGraph (Fin k)), ¬ H.IsAcyclic →
      ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop,
        (numFree H n : ℝ) ≤ (2 : ℝ) ^ (C * (extremalNumber n H : ℝ))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/59.lean, line 111.

Sources

• FormalConjectures/ErdosProblems/59.lean at 2055e5ad
• erdosproblems.com/59

LeanErdos59.erdos_59 · Erdos59.erdos_59.variants.erdos_frankl_rodl · Erdos59.erdos_59.variants.morris_saxton · Erdos59.erdos_59.variants.c4 · Erdos59.erdos_59.variants.big_o

TheoremErdős Problem 60#

References: - erdosproblems.com/60 - [HeMaYa21] He, J. and Ma, J. and Yang, T., Some extremal results on 4-cycles. Journal of Combinatorial Theory B (2021).

Quoted from FormalConjectures/ErdosProblems/60.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/60.

The file states 3 research or textbook statements: 1 open and 2 solved.

Erdos60.erdos_60

Open: stated without proof.

Does every graph on \(n\) vertices with \(>\mathrm{ex}(n;C_4)\) edges contain \(\gg n^{1/2}\) many copies of \(C_4\)?

theorem erdos_60 :
    ∃ c : ℝ, c > 0 ∧
      ∀ᶠ n : ℕ in atTop,
        ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
          (extremalNumber n (cycleGraph 4) < G.edgeFinset.card) →
          (c * Real.sqrt (n : ℝ) ≤ ({ H' : G.Subgraph | Nonempty (H'.coe ≃g cycleGraph 4) }.ncard : ℝ))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/60.lean, line 41.

Erdos60.erdos_60.variants.he_ma_yang

Solved: stated here without proof.

He, Ma, and Yang [HeMaYa21] proved the conjecture when \(n = q^2 + q + 1\) for some \(q = 2^k\): they showed that for large even \(q\) every graph on \(q^2 + q + 1\) vertices with \(\frac{1}{2}q(q+1)^2 + 1\) edges contains at least \(q - 1\) copies of \(C_4\), and \(\mathrm{ex}(q^2 + q + 1; C_4) = \frac{1}{2}q(q+1)^2\) when \(q = 2^k\).

theorem erdos_60.variants.he_ma_yang :
    ∃ c : ℝ, c > 0 ∧
      ∀ (q : ℕ) (_hq : q.isPowerOfTwo),
        ∀ (G : SimpleGraph (Fin (q^2 + q + 1))) [DecidableRel G.Adj],
          (extremalNumber (q^2 + q + 1) (cycleGraph 4) < G.edgeFinset.card) →
          (c * Real.sqrt ((q^2 + q + 1) : ℝ) ≤ ({ H' : G.Subgraph | Nonempty (H'.coe ≃g cycleGraph 4) }.ncard : ℝ))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/60.lean, line 58.

Erdos60.erdos_60.variants.two_copies

Solved: stated here without proof.

Erdős and Simonovits conjectured that at least 2 copies of \(C_4\) are guaranteed.

theorem erdos_60.variants.two_copies :
    ∀ᶠ n : ℕ in atTop,
      ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
        (extremalNumber n (cycleGraph 4) < G.edgeFinset.card) →
        (2 ≤ { H' : G.Subgraph | Nonempty (H'.coe ≃g cycleGraph 4) }.ncard)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/60.lean, line 70.

Sources

• FormalConjectures/ErdosProblems/60.lean at 2055e5ad
• erdosproblems.com/60

LeanErdos60.erdos_60 · Erdos60.erdos_60.variants.he_ma_yang · Erdos60.erdos_60.variants.two_copies

TheoremErdős Problem 61 -- Erdős–Hajnal Conjecture#

Reference: erdosproblems.com/61

Quoted from FormalConjectures/ErdosProblems/61.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/61.

The file states 5 research or textbook statements: 1 open and 4 solved.

Erdos61.erdos_61

Open: stated without proof.

The Erdős–Hajnal Conjecture states that there is a constant \(c(H) > 0\) for each \(H\) such that we can take \(f(n) = n^{c(H)}\) in the above formulation.

theorem erdos_61 :
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => (n : ℝ) ^ c)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/61.lean, line 49.

Erdos61.erdos_61.variants.erha89

Solved: stated here without proof.

Erdős and Hajnal [ErHa89] proved that we can take \(f(n) = \exp(c_H \sqrt{\log n})\) for some constant \(c_H > 0\) depending on \(H\).

[ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.

theorem erdos_61.variants.erha89 :
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => exp (c * sqrt (log n)))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/61.lean, line 61.

Erdos61.erdos_61.variants.bnss23

Solved: stated here without proof.

Bucić, Nguyen, Scott, and Seymour [BNSS23] improved this to \(f(n) = \exp(c_H \sqrt{\log n \log \log n})\) for some constant \(c_H > 0\) depending on \(H\).

[BNSS23] Bucić, M. and Nguyen, T. and Scott, A. and Seymour, P., A loglog step towards Erdos-Hajnal

theorem erdos_61.variants.bnss23 :
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => exp (c * sqrt (log n * log (log n))))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/61.lean, line 73.

Erdos61.erdos_61.variants.p5

Solved: stated here without proof.

Nguyen, Scott, and Seymour [NSS23] proved the conjecture for \(H = P_5\), the path on five vertices: every \(P_5\)-free graph on \(n\) vertices has a clique or independent set of polynomial size.

[NSS23] Nguyen, T., Scott, A. and Seymour, P., Induced subgraph density. VII. The five-vertex path. arXiv:2312.15333

theorem erdos_61.variants.p5 :
    ∃ c > (0 : ℝ), IsErdosHajnalLowerBound (pathGraph 5) (fun n : ℕ => (n : ℝ) ^ c)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/61.lean, line 87.

Erdos61.erdos_61.variants.c5

Solved: stated here without proof.

Chudnovsky, Scott, Seymour, and Spirkl [CSSS23] proved the conjecture for \(H = C_5\), the cycle on five vertices: every graph with no induced five-cycle has a clique or independent set of polynomial size.

[CSSS23] Chudnovsky, M., Scott, A., Seymour, P. and Spirkl, S., Erdős–Hajnal for graphs with no 5-hole. Proc. Lond. Math. Soc. (3) 126 (2023), 997–1014.

theorem erdos_61.variants.c5 :
    ∃ c > (0 : ℝ), IsErdosHajnalLowerBound (cycleGraph 5) (fun n : ℕ => (n : ℝ) ^ c)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/61.lean, line 100.

Sources

• FormalConjectures/ErdosProblems/61.lean at 2055e5ad
• erdosproblems.com/61

LeanErdos61.erdos_61 · Erdos61.erdos_61.variants.erha89 · Erdos61.erdos_61.variants.bnss23 · Erdos61.erdos_61.variants.p5 · Erdos61.erdos_61.variants.c5

TheoremErdős Problem 63#

References: - erdosproblems.com/63 - [dBEr51] de Bruijn, N. G. and Erdős, P., A colour problem for infinite graphs and a problem in the theory of relations. Indag. Math. (1951), 369--373. - [ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99. - [LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020). - [Re24] Reiher, C., Graphs of large girth. arXiv:2403.13571 (2024).

Quoted from FormalConjectures/ErdosProblems/63.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/63.

The file states 1 research or textbook statement: 1 solved.

Erdos63.erdos_63

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos63.lean#L46.

Does every graph with infinite chromatic number contain a cycle of length \(2^n\) for infinitely many \(n\)?

Conjectured by Mihók and Erdős. Solved affirmatively following the work of Liu and Montgomery [LiMo20].

The linked formal proof (Codex) states the conclusion as {n | HasCycleLength G (2 ^ n)}.Infinite, with HasCycleLength G m unfolding to m ∈ G.cycleLengths.

theorem erdos_63 :
    ∀ {V : Type*} (G : SimpleGraph V), G.chromaticNumber = ⊤ →
      ∀ N : ℕ, ∃ n ≥ N, 2 ^ n ∈ G.cycleLengths

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/63.lean, line 51.

Sources

• FormalConjectures/ErdosProblems/63.lean at 2055e5ad
• erdosproblems.com/63

LeanErdos63.erdos_63

TheoremErdős Problem 64#

Reference: erdosproblems.com/64

Quoted from FormalConjectures/ErdosProblems/64.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/64.

The file states 1 research or textbook statement: 1 open.

Erdos64.erdos_64

Open: stated without proof.

Does every finite graph with minimum degree at least \(3\) contain a cycle of length \(2^k\) for some \(k \geq 2\)?

theorem erdos_64 :
    ∀ (V : Type*) (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj],
        G.minDegree ≥ 3 → ∃ (k : ℕ) (v : V) (c : G.Walk v v),
            k ≥ 2 ∧ c.IsCycle ∧ c.length = 2^k

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/64.lean, line 35.

Sources

• FormalConjectures/ErdosProblems/64.lean at 2055e5ad
• erdosproblems.com/64

LeanErdos64.erdos_64

TheoremErdős Problem 65#

References: - erdosproblems.com/65 - [GKS84] Gyárfás, A., Komlós, J. and Szemerédi, E., On the distribution of cycle lengths in graphs. J. Graph Theory (1984), 441-462. - [GPSV85] Gyárfás, A., Prömel, H. J., Szemerédi, E. and Voigt, B., On the sum of the reciprocals of cycle lengths in sparse graphs. Combinatorica (1985), 41-52. - [LiMo20] Liu, H. and Montgomery, R., A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).

Quoted from FormalConjectures/ErdosProblems/65.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/65.

The file states 3 research or textbook statements: 1 open and 2 solved.

Erdos65.erdos_65.parts.i

Solved: stated here without proof.

Let \(G\) be a graph with \(n\) vertices and \(kn\) edges, and \(a_1\lt a_2\lt \cdots\) be the lengths of cycles in \(G\). Assume \(n>0\). Is it true that

\[\sum\frac{1}{a_i}\gg \log k?\]

Gyárfás, Komlós, and Szemerédi [GKS84] have proved that this sum is \(\gg \log k\), so that only the second question remains.

The bound is stated for all sufficiently large \(k\): [GKS84, Theorem 4'] proves it for \(k \geq b\), where \(b\) is a constant. The case of \(k\) slightly larger than \(1\) is a separate problem, studied in [GPSV85].

theorem erdos_65.parts.i :
    ∃ c > (0 : ℝ), ∀ᶠ k : ℝ in Filter.atTop,
      ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V),
        0 < n →
        Fintype.card V = n →
        (G.edgeSet.ncard : ℝ) = k * n →
        (∑ᶠ a ∈ G.cycleLengths, (1 : ℝ) / a) ≥ c * Real.log k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/65.lean, line 50.

Erdos65.erdos_65.parts.ii

Open: stated without proof.

Is the sum \(\sum\frac{1}{a_i}\) minimised when \(G\) is a complete bipartite graph?

This problem is #65 in Extremal Graph Theory in the graphs problem collection.

theorem erdos_65.parts.ii :
    ∀ (k : ℝ) (hk : 0 < k),
      ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V),
        0 < n →
        Fintype.card V = n →
        (G.edgeSet.ncard : ℝ) = k * n →
        ∀ (A B : Type) [Fintype A] [Fintype B],
          Fintype.card (A ⊕ B) = n →
          ((completeBipartiteGraph A B).edgeSet.ncard : ℝ) = k * n →
          (∑ᶠ a ∈ (completeBipartiteGraph A B).cycleLengths, (1 : ℝ) / a) ≤
            (∑ᶠ a ∈ G.cycleLengths, (1 : ℝ) / a)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/65.lean, line 65.

Erdos65.erdos_65.variants.liu_montgomery

Solved: stated here without proof.

Liu and Montgomery [LiMo20, Corollary 1.2] have proved the asymptotically sharp lower bound of \(\geq (\tfrac{1}{2}-o(1))\log k\).

theorem erdos_65.variants.liu_montgomery :
    ∀ ε > (0 : ℝ), ∀ᶠ k : ℝ in Filter.atTop,
      ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V),
        0 < n →
        Fintype.card V = n →
        (G.edgeSet.ncard : ℝ) = k * n →
        (∑ᶠ a ∈ G.cycleLengths, (1 : ℝ) / a) ≥ (1 / 2 - ε) * Real.log k

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/65.lean, line 83.

Sources

• FormalConjectures/ErdosProblems/65.lean at 2055e5ad
• erdosproblems.com/65

LeanErdos65.erdos_65.parts.i · Erdos65.erdos_65.parts.ii · Erdos65.erdos_65.variants.liu_montgomery

TheoremErdős Problem 66#

Reference: erdosproblems.com/66

Quoted from FormalConjectures/ErdosProblems/66.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/66.

The file states 1 research or textbook statement: 1 open.

Erdos66.erdos_66

Open: stated without proof.

Is there and \(A \subset \mathbb{N}\) is such that

\[\lim_{n\to \infty}\frac{1_A\ast 1_A(n)}{\log n}\]

exists and is \(\ne 0\)?

theorem erdos_66 : ∃ (A : Set ℕ) (c : ℝ), c ≠ 0 ∧
    Tendsto (fun n ↦ (sumRep A n : ℝ) / Real.log n) atTop (𝓝 c)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/66.lean, line 40.

Sources

• FormalConjectures/ErdosProblems/66.lean at 2055e5ad
• erdosproblems.com/66

LeanErdos66.erdos_66

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.