Erdős Problem 22 to Erdős Problem 43

TheoremErdős Problem 22#

The central problem of Ramsey–Turán theory: writing \(\mathrm{rt}(n; k, \ell)\) for the maximum number of edges of a \(K_k\)-free graph on \(n\) vertices whose largest independent set has size less than \(\ell\), is it true that for every \(\epsilon > 0\) and all sufficiently large \(n\)

\[\mathrm{rt}(n; 4, \epsilon n) \geq n^2/8?\]

Conjectured by Bollobás and Erdős [BoEr76], who constructed such a graph with \((1/8 + o(1))n^2\) edges. Together with the matching upper bound \(\mathrm{rt}(n; 4, \epsilon n) \leq (1/8 + o(1))n^2\) of Szemerédi [Sz72], this determines the Ramsey–Turán density of \(K_4\) to be \(1/8\). The conjecture as stated was proved by Fox, Loh, and Zhao [FLZ15].

References: * erdosproblems.com/22 * [BoEr76] Bollobás, B. and Erdős, P., On a Ramsey-Turán type problem. J. Combin. Theory Ser. B 21 (1976), 166--168. * [Sz72] Szemerédi, E., On graphs containing no complete subgraph with 4 vertices (Hungarian). Mat. Lapok 23 (1972), 113--116. * [FLZ15] Fox, J., Loh, P.-S., and Zhao, Y., The critical window for the classical Ramsey-Turán problem. Combinatorica 35 (2015), 435--476.

Quoted from FormalConjectures/ErdosProblems/22.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/22.

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

Erdos22.erdos_22

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

Let \(\epsilon > 0\) and let \(n\) be sufficiently large depending on \(\epsilon\). Is there a graph on \(n\) vertices with at least \(n^2/8\) many edges which contains no \(K_4\), such that the largest independent set has size at most \(\epsilon n\)?

This is true, as proved by Fox, Loh, and Zhao [FLZ15].

theorem erdos_22 :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ (n : ℕ) in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
        (G.indepNum : ℝ) ≤ ε * n ∧ (n : ℝ) ^ 2 / 8 ≤ G.edgeFinset.card

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

Erdos22.erdos_22.variants.szemeredi_upper

Solved: stated here without proof.

The matching upper bound, due to Szemerédi [Sz72]: a \(K_4\)-free graph on \(n\) vertices whose independence number is sublinear in \(n\) has at most \((1/8 + o(1))n^2\) edges. That is, for every \(\epsilon > 0\) there is a \(\delta > 0\) such that for all sufficiently large \(n\), every \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \leq \delta n\) has at most \((1/8 + \epsilon)n^2\) edges.

theorem erdos_22.variants.szemeredi_upper (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ (n : ℕ) in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
        (G.indepNum : ℝ) ≤ δ * n →
        (G.edgeFinset.card : ℝ) ≤ (1 / 8 + ε) * n ^ 2

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

Erdos22.erdos_22.variants.bollobas_erdos_lower

Solved: stated here without proof.

The construction of Bollobás and Erdős [BoEr76]: for every \(\epsilon > 0\) and \(\delta > 0\), for all sufficiently large \(n\) there is a \(K_4\)-free graph on \(n\) vertices with independence number at most \(\delta n\) and at least \((1/8 - \epsilon)n^2\) edges. Together with erdos_22.variants.szemeredi_upper this shows that the Ramsey–Turán density of \(K_4\) is \(1/8\).

theorem erdos_22.variants.bollobas_erdos_lower (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∀ᶠ (n : ℕ) in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
        (G.indepNum : ℝ) ≤ δ * n ∧ (1 / 8 - ε) * n ^ 2 ≤ G.edgeFinset.card

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

Erdos22.erdos_22.variants.fox_loh_zhao

Solved: stated here without proof.

The quantitative strengthening proved by Fox, Loh, and Zhao [FLZ15]: there is a constant \(C > 0\) such that for all sufficiently large \(n\) there exists a \(K_4\)-free graph on \(n\) vertices with at least \(n^2/8\) edges whose largest independent set has size at most

\[C \cdot \frac{(\log\log n)^{3/2}}{(\log n)^{1/2}} \cdot n.\]

theorem erdos_22.variants.fox_loh_zhao :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ (n : ℕ) in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
        (G.indepNum : ℝ) ≤
          C * (Real.log (Real.log n)) ^ (3 / 2 : ℝ) / (Real.log n) ^ (1 / 2 : ℝ) * n ∧
        (n : ℝ) ^ 2 / 8 ≤ G.edgeFinset.card

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

Sources

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

LeanErdos22.erdos_22 · Erdos22.erdos_22.variants.szemeredi_upper · Erdos22.erdos_22.variants.bollobas_erdos_lower · Erdos22.erdos_22.variants.fox_loh_zhao

TheoremErdős Problem 23#

References: * erdosproblems.com/23 * OEIS A389646 * Balogh-Clemen-Lidicky, Max Cuts in Triangle-free Graphs * McKay, Extremal graphs for bipartization of triangle-free graphs

Quoted from FormalConjectures/ErdosProblems/23.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/23.

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

Erdos23.erdos_23.variants.n5

Solved: stated here without proof.

Every triangle-free graph on \(25\) vertices can be made bipartite by removing at most \(25\) edges.

This is the \(n = 5\) case of Erdős Problem 23. It follows from the high-density range of Balogh-Clemen-Lidicky together with McKay's complete catalogue of the 23-vertex extremal graphs for bipartization of triangle-free graphs.

theorem erdos_23.variants.n5 :
    ∀ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 → ∃ (H : SimpleGraph (Fin 25)),
        H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 25

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

Erdos23.erdos_23.variants.n5_tight

Solved: stated here without proof.

There exists a triangle-free graph on \(25\) vertices such that at least \(25\) edges must be removed to make it bipartite. The balanced blow-up of \(C_5\) with five parts of size \(5\) witnesses this.

theorem erdos_23.variants.n5_tight :
    ∃ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 ∧ ∀ (H : SimpleGraph (Fin 25)),
        H ≤ G → H.IsBipartite → 25 ≤ (G.edgeFinset \ H.edgeFinset).card

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

Erdos23.erdos_23

Open: stated without proof.

Can every triangle-free graph on \(5n\) vertices be made bipartite by deleting at most \(n^2\) edges?

theorem erdos_23 :
    ∀ (n : ℕ) (V : Type) [Fintype V], Fintype.card V = 5 * n →
      ∀ (G : SimpleGraph V), G.CliqueFree 3 →
        ∃ (H : SimpleGraph V),
          H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ n^2

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

Sources

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

LeanErdos23.erdos_23.variants.n5 · Erdos23.erdos_23.variants.n5_tight · Erdos23.erdos_23

TheoremErdős Problem 24#

References: - erdosproblems.com/24 - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [Gr12] Grzesik, Andrzej, On the maximum number of five-cycles in a triangle-free graph. J. Combin. Theory Ser. B (2012), 1061-1066. - [HHKNR13] Hatami, Hamed and Hladký, Jan and Kráľ, Daniel and Norine, Serguei and Razborov, Alexander, On the number of pentagons in triangle-free graphs. J. Combin. Theory Ser. A (2013), 722-732.

Quoted from FormalConjectures/ErdosProblems/24.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/24.

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

Erdos24.erdos_24

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

Does every triangle-free graph on \(5n\) vertices contain at most \(n^5\) copies of \(C_5\)?

Győri proved this with \(1.03n^5\), which has been improved by Füredi. The answer is yes, as proved independently by Grzesik [Gr12] and Hatami, Hladky, Král, Norine, and Razborov [HHKNR13].

theorem erdos_24 :
    ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 →
      G.copyCount (cycleGraph 5) ≤ n ^ 5

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

Sources

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

LeanErdos24.erdos_24

TheoremErdős Problem 25: Logarithmic density of size-dependent congruences#

Reference: erdosproblems.com/25

Quoted from FormalConjectures/ErdosProblems/25.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/25.

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

Erdos25.erdos_25

Open: stated without proof.

Let \(n_1 < n_2 < \dots\) be an arbitrary sequence of integers, each with an associated residue class \(a_i \pmod{n_i}\). Let \(A\) be the set of integers \(n\) such that for every \(i\) either \(n < n_i\) or \(n \not\equiv a_i \pmod{n_i}\). Must the logarithmic density of \(A\) exist?

theorem erdos_25 :
    ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ i, 0 < seq_n i) → StrictMono seq_n →
      ∃ d, Set.HasLogDensity
        { x : ℕ | ∀ i, (x : ℤ) < seq_n i ∨ ¬((x : ℤ) ≡ seq_a i [ZMOD seq_n i]) } d

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

Sources

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

LeanErdos25.erdos_25

TheoremErdős Problem 26#

References: - erdosproblems.com/26 - Te19 G. Tenenbaum, Some of Erdős' unconventional problems in number theory, thirty-four years later, arXiv:1908.00488 [math.NT] (2019)

Quoted from FormalConjectures/ErdosProblems/26.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/26.

The file states 3 research or textbook statements: 3 solved. It also has 7 test statements, counted here but not shown.

Erdos26.erdos_26

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

Let \(A\subset\mathbb{N}\) be infinite such that \(\sum_{a \in A} \frac{1}{a} = \infty\). Must there exist some \(k\geq 1\) such that almost all integers have a divisor of the form \(a+k\) for some \(a\in A\)?

This was formalized in Lean by Alexeev using Aristotle.

theorem erdos_26 : ¬ ∀ A : ℕ → ℕ, StrictMono A → IsThick A →
    ∃ k, IsBehrend (A · + k)

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

Erdos26.erdos_26.variants.rusza

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

If we allow for \(\sum_{a\in A} \frac{1}{a} < \infty\) then Rusza has found a counter-example.

theorem erdos_26.variants.rusza : ∃ A : ℕ → ℕ,
    StrictMono A ∧ ¬IsThick A ∧ ∀ k, ¬IsBehrend (A · + k)

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

Erdos26.erdos_26.variants.tenenbaum

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/09c54540aa51cb40dff73660c94a82e2631386f8/FormalConjectures/ErdosProblems/26.lean#L625.

Tenenbaum asked the weaker variant where for every \(\epsilon>0\) there is some \(k=k(\epsilon)\) such that at least \(1-\epsilon\) density of all integers have a divisor of the form \(a+k\) for some \(a\in A\).

The DeepMind prover agent has found a formal disproof of this statement.

theorem erdos_26.variants.tenenbaum : ¬ ∀ᵉ (A : ℕ → ℕ), StrictMono A → IsThick A →
    (∀ ε > (0 : ℝ), ∃ k, IsWeaklyBehrend (A · + k) ε)

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

Sources

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

LeanErdos26.erdos_26 · Erdos26.erdos_26.variants.rusza · Erdos26.erdos_26.variants.tenenbaum

TheoremErdős Problem 28#

Reference: erdosproblems.com/28

Quoted from FormalConjectures/ErdosProblems/28.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/28.

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

Erdos28.erdos_28

Open: stated without proof.

If \(A ⊆ \mathbb{N}\) is such that \(A + A\) contains all but finitely many integers then \(\limsup 1_A ∗ 1_A(n) = \infty\).

theorem erdos_28 (A : Set ℕ) (h : (A + A)ᶜ.Finite) :
    limsup (fun (n : ℕ) => (sumRep A n : ℕ∞)) atTop = (⊤ : ℕ∞)

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

Sources

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

LeanErdos28.erdos_28

TheoremErdős Problem 29#

References: - erdosproblems.com/29 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er89d] Erdős, P., Some old and new problems on additive and combinatorial number theory. Combinatorial Mathematics: Proceedings of the Third International Conference (New York, 1985) (1989), 181-186. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [JPSZ24] Jain, V. and Pham, H. T. and Sawhney, M. and Zakharov, D., An explicit economical additive basis. arXiv:2405.08650 (2024).

Quoted from FormalConjectures/ErdosProblems/29.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/29.

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

Erdos29.erdos_29

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

Is there an explicit construction of a set \(A\subseteq \mathbb{N}\) such that \(A+A=\mathbb{N}\) but \(1_A\ast 1_A(n)=o(n^\epsilon)\) for every \(\epsilon>0\)?

The existence of such a set was asked by Sidon to Erdős in 1932. Erdős (eventually) proved the existence of such a set using probabilistic methods. This problem asks for a constructive solution. An explicit construction was given by Jain, Pham, Sawhney, and Zakharov [JPSZ24].

The formal statement records the existence of such a set; the linked formal proof exhibits an explicit construction.

theorem erdos_29 : ∃ A : Set ℕ, A + A = Set.univ ∧ ∀ ε : ℝ, 0 < ε →
    (fun n : ℕ => (sumRep A n : ℝ)) =o[atTop] fun n : ℕ => (n : ℝ) ^ ε

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

Sources

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

LeanErdos29.erdos_29

TheoremErdős Problem 30#

References: - erdosproblems.com/30 - [ErTu41] Erdős, P. and Turán, P., On a problem of Sidon in additive number theory, and on some related problems. J. London Math. Soc. 16 (1941), 212-215. - [Li69] Lindström, B., An inequality for \(B_2\)-sequences. J. Combinatorial Theory 6 (1969), 211-212. - [Si38] Singer, J., A theorem in finite projective geometry and some applications to number theory. Trans. Amer. Math. Soc. 43 (1938), 377-385. - [BFR23] Balogh, J., Füredi, Z. and Roy, S., An upper bound on the size of Sidon sets. Amer. Math. Monthly 130 (2023), 437-445. - [OB22] O'Bryant, K., On the size of finite Sidon sets. arXiv:2207.07800 (2022). - [CHO25] Carter, D., Hunter, Z. and O'Bryant, K., On the diameter of finite Sidon sets. Acta Math. Hungar. 175 (2025), 108-126.

See also Ben Green's Open Problem 31 (formalised in FormalConjectures/GreensOpenProblems/31.lean).

Quoted from FormalConjectures/ErdosProblems/30.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/30.

The file states 14 research or textbook statements: 2 open, 7 solved and 5 textbook results.

Erdos30.erdos_30

Open: stated without proof.

Is it true that, for every \(\varepsilon > 0\), \(h(N) = \sqrt N + O_{\varepsilon}(N^\varepsilon)\)

theorem erdos_30 :
    ∀ᵉ (ε > 0), (fun N => h N - (N : Real).sqrt) =O[atTop] fun N => (N : ℝ)^(ε : ℝ)

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

Erdos30.erdos_30.variants.O_one

Open: stated without proof.

A stronger conjecture: is it true that \(h(N) = \sqrt N + O(1)\)? Erdős thought this was perhaps too optimistic.

theorem erdos_30.variants.O_one :
    (fun N => h N - (N : ℝ).sqrt) =O[atTop] fun _ => (1 : ℝ)

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

Erdos30.erdos_30.variants.erdos_turan

Solved: stated here without proof.

Erdős and Turán [ErTu41] proved \(h(N) \le \sqrt N + O(N^{1/4})\).

This is an upper bound only. A statement with =O would also assert the lower bound \(h(N) \ge \sqrt N - O(N^{1/4})\), which is not part of this result.

theorem erdos_30.variants.erdos_turan :
    ∃ C : ℝ, ∀ᶠ N in atTop, (h N : ℝ) ≤ (N : ℝ).sqrt + C * (N : ℝ) ^ (4⁻¹ : ℝ)

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

Erdos30.erdos_30.variants.lindstrom

Solved: stated here without proof.

The proofs of Erdős–Turán [ErTu41] and Lindström [Li69] in fact give, for all \(N\), \(h(N) \le N^{1/2} + N^{1/4} + 1\).

theorem erdos_30.variants.lindstrom (N : ℕ) :
    (h N : ℝ) ≤ (N : ℝ).sqrt + (N : ℝ) ^ (4⁻¹ : ℝ) + 1

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

Erdos30.erdos_30.variants.balogh_furedi_roy

Solved: stated here without proof.

Balogh, Füredi and Roy [BFR23] proved \(h(N) \le N^{1/2} + 0.998 N^{1/4}\) for all sufficiently large \(N\).

theorem erdos_30.variants.balogh_furedi_roy :
    ∀ᶠ N in atTop, (h N : ℝ) ≤ (N : ℝ).sqrt + (0.998 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ)

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

Erdos30.erdos_30.variants.obryant

Solved: stated here without proof.

O'Bryant [OB22] proved \(h(N) \le N^{1/2} + 0.99703 N^{1/4}\) for all sufficiently large \(N\).

theorem erdos_30.variants.obryant :
    ∀ᶠ N in atTop, (h N : ℝ) ≤ (N : ℝ).sqrt + (0.99703 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ)

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

Erdos30.erdos_30.variants.carter_hunter_obryant

Solved: stated here without proof.

Carter, Hunter and O'Bryant [CHO25] proved \(h(N) \le N^{1/2} + 0.98183 N^{1/4} + O(1)\). This is the current record upper bound.

theorem erdos_30.variants.carter_hunter_obryant :
    ∃ C : ℝ, ∀ᶠ N in atTop,
      (h N : ℝ) ≤ (N : ℝ).sqrt + (0.98183 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C

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

Erdos30.erdos_30.variants.singer

Solved: stated here without proof.

Singer's construction [Si38] shows \(h(N) \ge (1 - o(1)) N^{1/2}\) for all \(N\).

theorem erdos_30.variants.singer :
    ∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop, (1 - ε) * (N : ℝ).sqrt ≤ h N

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

Erdos30.erdos_30.variants.isEquivalent_sqrt

Solved: stated here without proof.

Combining Singer's lower bound [Si38] with the Erdős–Turán upper bound [ErTu41]: \(h(N) \sim N^{1/2}\).

theorem erdos_30.variants.isEquivalent_sqrt :
    (fun N => (h N : ℝ)) ~[atTop] fun N => (N : ℝ).sqrt

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

Erdos30.erdos_30.variants.elementary_difference_count

Textbook result, proved here.

The counting argument of Erdős and Turán [ErTu41]: a Sidon set \(A \subseteq \{0, \dots, N\}\) has \(|A|(|A| - 1) \le 2N\), because the \(|A|(|A|-1)/2\) positive differences of \(A\) are distinct and lie in \(\{1, \dots, N\}\).

theorem erdos_30.variants.elementary_difference_count (A : Finset ℕ) (N : ℕ)
    (hS : IsSidon (A : Set ℕ)) (hA : A ⊆ Finset.range (N + 1)) :
    A.card * (A.card - 1) ≤ 2 * N

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/30.lean, line 142.

Erdos30.erdos_30.variants.distinct_sums_card

Textbook result, proved here.

For a Sidon set \(A\), \(|A + A| = |A|(|A|+1)/2\): the sums \(a + b\) with \(a \le b\) are pairwise distinct [ErTu41].

theorem erdos_30.variants.distinct_sums_card (A : Finset ℕ) (hS : IsSidon (A : Set ℕ)) :
    (A + A).card = A.card * (A.card + 1) / 2

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/30.lean, line 165.

Erdos30.erdos_30.variants.distinct_sums_in_range

Textbook result, proved here.

If \(A \subseteq \{0, \dots, N\}\) then \(A + A \subseteq \{0, \dots, 2N\}\).

theorem erdos_30.variants.distinct_sums_in_range (A : Finset ℕ) (N : ℕ)
    (hA : A ⊆ Finset.range (N + 1)) :
    A + A ⊆ Finset.range (2 * N + 1)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/30.lean, line 199.

Erdos30.erdos_30.variants.erdos_turan_counting

Textbook result, proved here.

The counting bound of Erdős and Turán [ErTu41] in its sum form: a Sidon set \(A \subseteq \{0, \dots, N\}\) has \(|A|(|A| + 1)/2 \le 2N + 1\).

theorem erdos_30.variants.erdos_turan_counting (A : Finset ℕ) (N : ℕ)
    (hS : IsSidon (A : Set ℕ)) (hA : A ⊆ Finset.range (N + 1)) :
    A.card * (A.card + 1) / 2 ≤ 2 * N + 1

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/30.lean, line 210.

Erdos30.erdos_30.variants.lindstrom_weak

Textbook result, proved here.

A weak form of Lindström's bound [Li69], following from erdos_30.variants.elementary_difference_count: a Sidon set \(A \subseteq \{0, \dots, N\}\) has \(|A| \le \lfloor \sqrt{2N} \rfloor + 1\).

theorem erdos_30.variants.lindstrom_weak (A : Finset ℕ) (N : ℕ)
    (hS : IsSidon (A : Set ℕ)) (hA : A ⊆ Finset.range (N + 1)) :
    A.card ≤ Nat.sqrt (2 * N) + 1

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/30.lean, line 222.

Sources

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

LeanErdos30.erdos_30 · Erdos30.erdos_30.variants.O_one · Erdos30.erdos_30.variants.erdos_turan · Erdos30.erdos_30.variants.lindstrom · Erdos30.erdos_30.variants.balogh_furedi_roy · Erdos30.erdos_30.variants.obryant · Erdos30.erdos_30.variants.carter_hunter_obryant · Erdos30.erdos_30.variants.singer · Erdos30.erdos_30.variants.isEquivalent_sqrt · Erdos30.erdos_30.variants.elementary_difference_count · Erdos30.erdos_30.variants.distinct_sums_card · Erdos30.erdos_30.variants.distinct_sums_in_range · Erdos30.erdos_30.variants.erdos_turan_counting · Erdos30.erdos_30.variants.lindstrom_weak

TheoremErdős Problem 31#

References: - erdosproblems.com/31 - [Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137. - [Er59] Erdős, P., Über einige Probleme der additiven Zahlentheorie. Sammelband zu Ehren des 250. Geburtstages Leonhard Eulers (1959), 116-119. - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [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. - [Lo54] Lorentz, G. G., On a problem of additive number theory. Proc. Amer. Math. Soc. (1954), 838-841.

Quoted from FormalConjectures/ErdosProblems/31.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/31.

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

Erdos31.erdos_31

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

Given any infinite set \(A\subset \mathbb{N}\) there is a set \(B\) of density \(0\) such that \(A+B\) contains all except finitely many integers.

Conjectured by Erdős and Straus. Proved by Lorentz [Lo54].

theorem erdos_31 : ∀ A : Set ℕ, A.Infinite →
    ∃ B : Set ℕ, B.HasDensity 0 ∧ ∀ᶠ n in atTop, n ∈ A + B

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

Sources

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

LeanErdos31.erdos_31

TheoremErdős Problem 32#

References: * erdosproblems.com/32 * [Erd54] Erdős, Paul, Some results on additive number theory. Proc. Amer. Math. Soc. (1954), 847-853. * [Guy04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437 * [Ru98c] Ruzsa, Imre Z., On the additive completion of primes. Acta Arith. (1998), 269-275.

Quoted from FormalConjectures/ErdosProblems/32.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/32.

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

Erdos32.erdos_32.variants.log_squared

Solved: stated here without proof.

Erdős proved in [Erd54] that there exists an additive complement \(A\) to the primes with \(|A \cap \{1, \ldots, N\}| = O((\log N)^2)\).

theorem erdos_32.variants.log_squared : ∃ A : Set ℕ,
    IsAdditiveComplementToPrimes A ∧
    (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card : ℝ)) =O[atTop]
      fun N => (Real.log N) ^ 2

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

Erdos32.erdos_32.variants.liminf_gt_one

Solved: stated here without proof.

Must every additive complement \(A\) to the primes satisfy \(\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} > 1\)?

theorem erdos_32.variants.liminf_gt_one : ∀ A : Set ℕ,
    IsAdditiveComplementToPrimes A →
    (1 : EReal) < liminf (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card / Real.log N : EReal))
      atTop

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

Erdos32.erdos_32

Open: stated without proof.

Does there exist a set \(A \subseteq \mathbb{N}\) such that \(|A \cap \{1, \ldots, N\}| = o((\log N)^2)\) and every sufficiently large integer can be written as \(p + a\) for some prime \(p\) and \(a \in A\)?

theorem erdos_32 : ∃ A : Set ℕ,
    IsAdditiveComplementToPrimes A ∧
    (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card : ℝ)) =o[atTop]
      fun N => (Real.log N) ^ 2

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

Erdos32.erdos_32.variants.log_bound

Open: stated without proof.

Can the bound \(O(\log N)\) be achieved for an additive complement to the primes? [Guy04] writes that Erdős offered $50 for the solution.

theorem erdos_32.variants.log_bound : ∃ A : Set ℕ,
    IsAdditiveComplementToPrimes A ∧
    (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card : ℝ)) =O[atTop]
      fun N => Real.log N

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

Erdos32.erdos_32.variants.ruzsa

Solved: stated here without proof.

Ruzsa proved that any additive complement \(A\) to the primes must satisfy \(\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} \geq e^\gamma\), where \(\gamma\) is the Euler-Mascheroni constant.

theorem erdos_32.variants.ruzsa : ∀ A : Set ℕ,
    IsAdditiveComplementToPrimes A →
    (Real.exp Real.eulerMascheroniConstant : EReal) ≤
      liminf (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card / Real.log N : EReal)) atTop

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

Sources

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

LeanErdos32.erdos_32.variants.log_squared · Erdos32.erdos_32.variants.liminf_gt_one · Erdos32.erdos_32 · Erdos32.erdos_32.variants.log_bound · Erdos32.erdos_32.variants.ruzsa

TheoremErdős Problem 33#

Reference: erdosproblems.com/33

Quoted from FormalConjectures/ErdosProblems/33.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/33.

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

Erdos33.erdos_33

Open: stated without proof.

Let A ⊆ ℕ be a set such that every integer can be written as n^2 + a for some a in A and n ≥ 0. What is the smallest possible value of lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2)?

theorem erdos_33 : ⨅ A : {A : Set ℕ | AdditiveBasisCondition A}, Filter.atTop.limsup (fun N =>
    (A.1 ∩ Icc 1 N).ncard / (√N : EReal)) = erdos_33.answer

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

Erdos33.erdos_33.variants.one_mem_lowerBounds

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/8c9a8ab727c1f06935b48a5ab4db145572cab9e9/erdos-33/Solution.lean#L70.

Erdos observed that this value is finite and > 1. This records the lower bound > 1, i.e. that 1 is a strict lower bound for every admissible A; the finiteness is erdos_33.variants.vanDoorn.

theorem erdos_33.variants.one_mem_lowerBounds :
    1 < ⨅ A : {A : Set ℕ | AdditiveBasisCondition A}, Filter.atTop.limsup (fun N =>
      (A.1 ∩ Icc 1 N).ncard / (√N : EReal))

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

Erdos33.erdos_33.variants.vanDoorn

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/8c9a8ab727c1f06935b48a5ab4db145572cab9e9/erdos-33/Solution.lean#L75.

The smallest possible value of lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) is at most 2φ^(5/2) ≈ 6.66, with φ equal to the golden ratio. Proven by Wouter van Doorn.

theorem erdos_33.variants.vanDoorn :
    ⨅ A : {A : Set ℕ | AdditiveBasisCondition A}, Filter.atTop.limsup (fun N =>
    (A.1 ∩ Icc 1 N).ncard / (√N : EReal)) ≤ ↑(2 * (φ ^ ((5 : ℝ) / 2)))

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

Sources

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

LeanErdos33.erdos_33 · Erdos33.erdos_33.variants.one_mem_lowerBounds · Erdos33.erdos_33.variants.vanDoorn

TheoremErdős Problem 34#

References: - erdosproblems.com/34 - [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). - [He86] Hegyvári, N., On consecutive sums in sequences. Acta Math. Hungar. (1986), 193--200. - [Ko15] Konieczny, J., On consecutive sums in permutations. arXiv:1504.07156 (2015).

Quoted from FormalConjectures/ErdosProblems/34.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/34.

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

Erdos34.erdos_34

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

For any permutation \(\pi\in S_n\) of \(\{1,\ldots,n\}\) let \(S(\pi)\) count the number of distinct consecutive sums, that is, sums of the shape \(\sum_{u\leq i\leq v}\pi(i)\). Is it true that

\[ S(\pi) = o(n^2) \]

for all \(\pi\in S_n\)?

Hegyvári [He86] gave a counterexample.

theorem erdos_34 :
    ¬ ∀ c : ℝ, 0 < c → ∃ N : ℕ, ∀ n ≥ N, ∀ p : Equiv.Perm (Fin n),
      ((consecutiveSums n p).card : ℝ) < c * (n : ℝ) ^ 2

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

Sources

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

LeanErdos34.erdos_34

TheoremErdős Problem 35#

References: - erdosproblems.com/35 - [Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137. - [Er36c] Erdős, P., On the arithmetical density of the sum of two sequences, one of which forms a basis for the integers. Acta. Arith. (1936), 197-200. - [Pl70] Plünnecke, H., Eine zahlentheoretische Anwendung der Graphentheorie. J. Reine. Angew. Math. (1970), 171-183.

Quoted from FormalConjectures/ErdosProblems/35.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/35.

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

Erdos35.erdos_35

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

Let \(B\subseteq\mathbb{N}\) be an additive basis of order \(k\) with \(0\in B\). Is it true that for every \(A\subseteq\mathbb{N}\) we have

\[d_s(A+B)\geq \alpha+\frac{\alpha(1-\alpha)}{k},\]

where \(\alpha=d_s(A)\) and

\[d_s(A) = \inf \frac{\lvert A\cap\{1,\ldots,N\}\rvert}{N}\]

is the Schnirelmann density?

Erdős [Er36c] proved this is true with \(k\) replaced by \(2k\) in the denominator (in a stronger form that only considers \(A\cup (A+b)\) for some \(b\in B\), see 38).

Ruzsa has observed that this follows immediately from the stronger fact proved by Plünnecke [Pl70] that (under the same assumptions, and for \(\alpha>0\))

\[d_S(A+B)\geq \alpha^{1-1/k}.\]

theorem erdos_35 : ∀ (B : Set ℕ) (k : ℕ), 0 ∈ B → B.IsAddBasisOfOrder k →
    ∀ A : Set ℕ, schnirelmannDensity A +
      schnirelmannDensity A * (1 - schnirelmannDensity A) / k ≤ schnirelmannDensity (A + B)

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

Erdos35.erdos_35.variants.plunnecke

Solved: stated here without proof.

Plünnecke [Pl70] proved that if \(B\subseteq\mathbb{N}\) is an additive basis of order \(k\) with \(0\in B\) then \(d_S(A+B)\geq d_s(A)^{1-1/k}\) for every \(A\subseteq\mathbb{N}\) with \(d_s(A)>0\).

theorem erdos_35.variants.plunnecke (B : Set ℕ) (k : ℕ) (h0 : 0 ∈ B) (hB : B.IsAddBasisOfOrder k)
    (A : Set ℕ) (hA : 0 < schnirelmannDensity A) :
    schnirelmannDensity A ^ (1 - (k : ℝ)⁻¹) ≤ schnirelmannDensity (A + B)

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

Sources

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

LeanErdos35.erdos_35 · Erdos35.erdos_35.variants.plunnecke

TheoremErdős Problem 36#

References: - erdosproblems.com/36 - Wikipedial: Minimum overlap problem

Quoted from FormalConjectures/ErdosProblems/36.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/36.

The file states 13 research or textbook statements: 3 open, 9 solved and 1 textbook result. It also has 5 test statements, counted here but not shown.

Erdos36.minimum_overlap.variants.lower.erdos_1955

Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/22db103d7b6109baca46f2623a7287b965a56936/erdos-36/Solution.lean#L52.

A lower bound of \(\frac 1 4\). See Some remarks on number theory (in Hebrew) by Paul Erdős, Riveon Lematematika 9, p.45-48,1955

theorem minimum_overlap.variants.lower.erdos_1955 :
    (1 : ℝ) / 4 ≤ atTop.liminf MinOverlapQuotient

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

Erdos36.minimum_overlap.variants.lower.scherk_1955

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/22db103d7b6109baca46f2623a7287b965a56936/erdos-36/Solution.lean#L56.

A lower bound of \(1 - frac{1}{\sqrt 2}\). Scherk (written communication), see On the minimal overlap problem of Erdös by Leo Moser, Аста Аrithmetica V, p. 117-119, 1959

theorem minimum_overlap.variants.lower.scherk_1955 :
    1 - (√2)⁻¹ < atTop.liminf MinOverlapQuotient

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

Erdos36.minimum_overlap.variants.lower.swierczkowski_1958

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/22db103d7b6109baca46f2623a7287b965a56936/erdos-36/Solution.lean#L60.

A lower bound of \(\frac{4 - \sqrt{6}}{5}\). See On the intersection of a linear set with the translation of its complement by Stanisław Świerczkowski1, Colloquium Mathematicum 5(2), p. 185-197, 1958

theorem minimum_overlap.variants.lower.swierczkowski_1958 :
    (4 - 6 ^ ((1 : ℝ) / 2)) / 5 < atTop.liminf MinOverlapQuotient

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

Erdos36.minimum_overlap.variants.lower.haugland_1996

Solved: stated here without proof.

A lower bound of \(\sqrt{4 - \sqrt{15}}\).

theorem minimum_overlap.variants.lower.haugland_1996 :
    (4 - 15 ^((1 : ℝ) / 2)) ^ ((1 : ℝ) / 2) < atTop.liminf MinOverlapQuotient

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

Erdos36.minimum_overlap.variants.lower.white_2022

Solved: stated here without proof.

A lower bound of \(0.379005\): the minimum overlap constant is at least \(0.379005\). See Erdős' minimum overlap problem by Ethan Patrick White, 2022

theorem minimum_overlap.variants.lower.white_2022 :
    0.379005 ≤ atTop.liminf MinOverlapQuotient

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

Erdos36.minimum_overlap.variants.upper.erdos_1955

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/22db103d7b6109baca46f2623a7287b965a56936/erdos-36/Solution.lean#L68.

The example (with \(N\) even), \(A = \{\frac N 2 + 1, \dots, \frac{3N}{2}\}\) shows an upper bound of \(\frac 1 2\).

theorem minimum_overlap.variants.upper.erdos_1955 :
    atTop.limsup MinOverlapQuotient ≤ (1 : ℝ) / 2

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

Erdos36.minimum_overlap.variants.upper.MRS_1956

Solved: stated here without proof.

An upper bound of \(\frac 2 5\). See Minimal overlapping under translation. by T. S. Motzkin, K. E. Ralston and J. L. Selfridge, in "The summer meeting in Seattle" by V. L. Klee Jr., Bull. Amer. Math. Soc.62, p. 558, 1956

theorem minimum_overlap.variants.upper.MRS_1956 :
    atTop.limsup MinOverlapQuotient ≤ (2 : ℝ) / 5

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

Erdos36.minimum_overlap.variants.upper.haugland_1996

Solved: stated here without proof.

An upper bound of \(0.38200298812318988\). See Advances in the Minimum Overlap Problem by Jan Kristian Haugland, Journal of Number Theory Volume 58, Issue 1, p 71-78, 1996

theorem minimum_overlap.variants.upper.haugland_1996 :
    atTop.limsup MinOverlapQuotient ≤ 0.38200298812318988

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

Erdos36.minimum_overlap.variants.upper.haugland_2022

Solved: stated here without proof.

An upper bound of \(0.3809268534330870\). See The minimum overlap problem by Jan Kristian Haugland

theorem minimum_overlap.variants.upper.haugland_2022 :
    atTop.limsup MinOverlapQuotient ≤ 0.3809268534330870

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

Erdos36.erdos_36.variants.lower

Open: stated without proof.

Find a better lower bound!

theorem erdos_36.variants.lower:
    ∃ (c : ℝ), 0.379005 < c ∧ c ≤ atTop.liminf MinOverlapQuotient ∧ c =
      erdos_36.variants.lower.answer

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

Erdos36.erdos_36.variants.upper

Open: stated without proof.

Find a better upper bound!

theorem erdos_36.variants.upper :
    ∃ (c : ℝ), c < 0.380926853433087 ∧ atTop.limsup MinOverlapQuotient ≤ c ∧ c =
      erdos_36.variants.upper.answer

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

Erdos36.erdos_36.variants.exists

Solved: stated here without proof.

The limit of MinOverlapQuotient exists and it is less than \(0.385694\).

theorem erdos_36.variants.exists : ∃ c, atTop.Tendsto MinOverlapQuotient (𝓝 c) ∧ c < 0.385694

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

Erdos36.erdos_36

Open: stated without proof.

Find the value of the limit of MinOverlapQuotient!

theorem erdos_36 : atTop.Tendsto MinOverlapQuotient (𝓝 erdos_36.answer)

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

Sources

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

LeanErdos36.minimum_overlap.variants.lower.erdos_1955 · Erdos36.minimum_overlap.variants.lower.scherk_1955 · Erdos36.minimum_overlap.variants.lower.swierczkowski_1958 · Erdos36.minimum_overlap.variants.lower.haugland_1996 · Erdos36.minimum_overlap.variants.lower.white_2022 · Erdos36.minimum_overlap.variants.upper.erdos_1955 · Erdos36.minimum_overlap.variants.upper.MRS_1956 · Erdos36.minimum_overlap.variants.upper.haugland_1996 · Erdos36.minimum_overlap.variants.upper.haugland_2022 · Erdos36.erdos_36.variants.lower · Erdos36.erdos_36.variants.upper · Erdos36.erdos_36.variants.exists · Erdos36.erdos_36

TheoremErdős Problem 38#

Reference: - erdosproblems.com/38 - [Er56](Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137.)

Quoted from FormalConjectures/ErdosProblems/38.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/38.

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

Erdos38.erdos_38

Solved: stated here; a Lean proof is at https://www.erdosproblems.com/forum/thread/38#post-6131.

Does there exist \(B \subset \mathbb{N}\) which is not an additive basis, but is such that for every set \(A \subseteq \mathbb{N}\) of Schnirelmann density \(\alpha\) and every \(N\) there exists \(b \in B\) such that

\[ \lvert (A \cup (A+b)) \cap \{1, \ldots, N\} \rvert \geq (\alpha + f(\alpha)) N \]

where \(f(\alpha) > 0\) for \(0 < \alpha < 1\)?

Note: here Erdős seems to use a slightly weaker notion of an additive basis (see [Er56] at the top of page 135). In particular, for this problem, a set is an additive basis of order \(k\) if every natural number can be written as a sum of at most \(k\) elements of the set, rather than as a sum of precisely \(k\) elements.

A positive solution was given by GPT 5.5 Pro (prompted by gebyjaff, cleanup by Liam Price); in fact a sparse random set \(B\) has this property, with \(f(\alpha)\gg \alpha (1-\alpha)^2\).

theorem erdos_38 :
    ∃ B : Set ℕ, ¬ B.IsWeakAddBasis ∧ ∃ f : ℝ → ℝ, (∀ α, 0 < α → α < 1 → f α > 0) ∧
      ∀ (A : Set ℕ) (N : ℕ),
        let α := schnirelmannDensity A
        ∃ b ∈ B, (Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * N

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

Sources

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

LeanErdos38.erdos_38

TheoremErdős Problem 39#

Reference: erdosproblems.com/39

Quoted from FormalConjectures/ErdosProblems/39.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/39.

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

Erdos39.erdos_39

Open: stated without proof.

Is there an infinite Sidon set \(A\subset \mathbb{N}\) such that \(\lvert A\cap \{1\ldots,N\}\rvert \gg_\epsilon N^{1/2-\epsilon}\) for all \(\varepsilon > 0\)?

theorem erdos_39 : ∃ (A : Set ℕ), A.Infinite ∧ IsSidon A ∧
    ∀ᵉ  (ε  > (0 : ℝ)),
    (· ^ (1 / 2 - ε) : ℕ → ℝ) =O[atTop] fun N => (((Set.Icc 1 N) ∩ A).ncard : ℝ)

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

Sources

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

LeanErdos39.erdos_39

TheoremErdős Problem 40#

Reference: erdosproblems.com/40

Quoted from FormalConjectures/ErdosProblems/40.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/40.

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

Erdos40.erdos_40

Open: stated without proof.

For what functions \(g(N) → \infty\) is it true that

\[\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}\]

implies \(\limsup 1_A\ast 1_A(n)=\infty\)?

theorem erdos_40 :
    {g : ℕ → ℝ | Tendsto g atTop atTop ∧ Erdos40For g} = erdos_40.answer

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

Erdos40.erdos_40.variants.weaker

Open: stated without proof.

Is there any function \(g(N) → \infty\) such that

\[\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}\]

implies \(\limsup 1_A\ast 1_A(n)=\infty\)?

This is a weaker form of Erdős Problem 40, which asks for all such \(g\). Establishing the implication for even one \(g(N) → \infty\) already answers Erdős Problem 28 positively, because a basis of order \(2\) satisfies \(\lvert A\cap \{1,\ldots,N\}\rvert \gg N^{1/2}\).

theorem erdos_40.variants.weaker :
    ∃ g : ℕ → ℝ, Tendsto g atTop atTop ∧ Erdos40For g

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

Erdos40.erdos_40.variants.implies_erdos_28

Textbook result, proved here.

Establishing the property in Erdős Problem 40 for any one function \(g(N) → \infty\) implies the Erdős-Turán conjecture, see Erdős Problem 28.

theorem erdos_40.variants.implies_erdos_28 (g : ℕ → ℝ) (hg : Tendsto g atTop atTop)
    (h_erdos_40 : Erdos40For g) : type_of% Erdos28.erdos_28

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/40.lean, line 76.

Sources

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

LeanErdos40.erdos_40 · Erdos40.erdos_40.variants.weaker · Erdos40.erdos_40.variants.implies_erdos_28

TheoremErdős Problem 41#

Reference: erdosproblems.com/41

Quoted from FormalConjectures/ErdosProblems/41.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/41.

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

Erdos41.erdos_41

Open: stated without proof.

Let \(A \subset \mathbb{N}\) be an infinite set such that the triple sums \(a+b+c\) are all distinct for \(a,b,c \in A\) (aside from the trivial coincidences). Is it true that

\[\liminf_{N \to \infty} \frac{\lvert A \cap \{1,\ldots,N\}\rvert}{N^{1/3}}=0?\]

theorem erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) :
    Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ)^(1/3 : ℝ)) = 0

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

Erdos41.erdos_41.variants.pairwise

Solved: stated here without proof.

Erdős proved that if the pairwise sums \(a+b\) are all distinct aside from the trivial coincidences, then

\[\liminf_{N \to \infty} \frac{\lvert A \cap \{1,\ldots,N\}\rvert}{N^{1/2}}=0.\]

theorem erdos_41.variants.pairwise (A : Set ℕ) (hA₂ : NtupleCondition A 2) (hA : A.Infinite) :
    Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ).sqrt) = 0

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

Sources

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

LeanErdos41.erdos_41 · Erdos41.erdos_41.variants.pairwise

TheoremErdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets#

Reference: erdosproblems.com/42

This problem asks whether maximal Sidon sets can coexist with other Sidon sets that have disjoint difference sets (apart from 0).

Quoted from FormalConjectures/ErdosProblems/42.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/42.

The file states 5 research or textbook statements: 2 solved and 3 textbook results.

Erdos42.erdos_42

Solved: stated here; a Lean proof is at https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P42/CompactCayley/Proof.lean.

Erdős Problem 42: Let M ≥ 1 and N be sufficiently large in terms of M. Is it true that for every maximal Sidon set A ⊆ {1,…,N} there is another Sidon set B ⊆ {1,…,N} of size M such that (A - A) ∩ (B - B) = {0}?

This was proved for all \(M\) by GPT 5.5 Pro (prompted by Sandhu), see discussion thread for more details.

theorem erdos_42 :
    ∀ M ≥ 1, ∀ᶠ N in atTop, ∀ (A : Set ℕ) (_ : IsMaximalSidonSetIn A N),
    ∃ᵉ (B : Set ℕ), B ⊆ Set.Icc 1 N ∧ IsSidon B ∧ B.ncard = M ∧
    ((A - A) ∩ (B - B)) = {0}

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

Erdos42.erdos_42.variants.constructive

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-42-constructive-variant/blob/1f82c76be43cb56f22e2f7f792e392d5fb3ff78c/lean/Erdos42Constructive.lean.

A variant asking for explicit bounds on how large N needs to be in terms of M.

This version provides a constructive function f such that for all M ≥ 1 and N ≥ f(M), every maximal Sidon set A ⊆ {1,…,N} has another Sidon set B ⊆ {1,…,N} of size M with disjoint difference sets (apart from 0).

theorem erdos_42.variants.constructive :
    ∃ (f : ℕ → ℕ), ∀ (M N : ℕ) (_ : 1 ≤ M) (_ : f M ≤ N),
    ∀ (A : Set ℕ) (_ : IsMaximalSidonSetIn A N), ∃ᵉ (B : Set ℕ),
      B ⊆ Set.Icc 1 N ∧ IsSidon B ∧ B.ncard = M ∧
      ((A - A) ∩ (B - B)) = {0}

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

Erdos42.example_maximal_sidon

Textbook result, proved here.

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

theorem example_maximal_sidon : IsMaximalSidonSetIn {1, 2, 4} 4

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

Erdos42.example_difference_set

Textbook result, proved here.

The difference set of {1, 2, 4} is {0, 1, 2, 3}.

theorem example_difference_set : ({1, 2, 4} : Set ℕ) - {1, 2, 4} = {0, 1, 2, 3}

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

Erdos42.maximal_sidon_contains_zero

Textbook result, proved here.

For any maximal Sidon set, the difference set contains 0.

theorem maximal_sidon_contains_zero (A : Set ℕ) (N : ℕ) (hN : 1 ≤ N)
    (hA : IsMaximalSidonSetIn A N) : 0 ∈ A - A

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

Sources

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

LeanErdos42.erdos_42 · Erdos42.erdos_42.variants.constructive · Erdos42.example_maximal_sidon · Erdos42.example_difference_set · Erdos42.maximal_sidon_contains_zero

TheoremErdős Problem 43#

Reference: erdosproblems.com/43

Quoted from FormalConjectures/ErdosProblems/43.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/43.

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

Erdos43.erdos_43.parts.i

Solved: stated here without proof.

If \(A\) and \(B\) are Sidon sets in \(\{1,\ldots,N\}\) with \((A-A)\cap(B-B)=\{0\}\), is it true that

\[\binom{\lvert A\rvert}{2}+\binom{\lvert B\rvert}{2}\leq\binom{f(N)}{2}+O(1)?\]

The answer is no; the Erdős Problems page notes that this follows from the solution to Erdős Problem 42.

theorem erdos_43.parts.i :
    ¬ ∃ C : ℝ, ∀ᶠ N in Filter.atTop, ∀ (A B : Finset ℕ),
      A ⊆ Finset.Icc 1 N →
      B ⊆ Finset.Icc 1 N →
      IsSidon (A : Set ℕ) →
      IsSidon (B : Set ℕ) →
      (A - A) ∩ (B - B) = {0} →
      ((A.card.choose 2 + B.card.choose 2 : ℕ) : ℝ) ≤ ((f N).choose 2 : ℝ) + C

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

Erdos43.erdos_43.parts.ii

Solved: stated here without proof.

If \(A\) and \(B\) are equal-sized Sidon sets in \(\{1,\ldots,N\}\) with \((A-A)\cap(B-B)=\{0\}\), can the bound be improved to

\[\binom{\lvert A\rvert}{2}+\binom{\lvert B\rvert}{2} \leq (1-c+o(1))\binom{f(N)}{2}\]

for some constant \(c>0\)?

The answer is no; the Erdős Problems page records a negative answer due to Barreto.

theorem erdos_43.parts.ii :
    ¬ ∃ᵉ (c > 0), ∃ o : ℕ → ℝ, o =o[Filter.atTop] (1 : ℕ → ℝ) ∧
    ∀ᶠ N in Filter.atTop, ∀ (A B : Finset ℕ),
      A ⊆ Finset.Icc 1 N →
      B ⊆ Finset.Icc 1 N →
      IsSidon (A : Set ℕ) →
      IsSidon (B : Set ℕ) →
      A.card = B.card →
      (A - A) ∩ (B - B) = {0} →
      ((A.card.choose 2 + B.card.choose 2 : ℕ) : ℝ) ≤
        (1 - c + o N) * ((f N).choose 2 : ℝ)

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

Sources

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

LeanErdos43.erdos_43.parts.i · Erdos43.erdos_43.parts.ii

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.