Erdős Problem 700 to Erdős Problem 722

TheoremErdős Problem 700#

Reference: erdosproblems.com/700

A problem of Erdős and Szekeres [ErSz78].

References: * [ErSz78] Erdős, P. and Szekeres, G., Some number theoretic problems on binomial coefficients, Austral. Math. Soc. Gaz. (1978), 97-99. * OEIS A091963 * Guy, R. K., Unsolved Problems in Number Theory, B31, B33.

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

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

Erdos700.erdos_700.parts.i

Open: stated without proof.

Let \(f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})\) and let \(P(n)\) be the largest prime dividing \(n\).

(a) Characterise those composite \(n\) such that \(f(n) = n/P(n)\).

Erdős–Szekeres [ErSz78] note that \(f(n) = n/P(n)\) when \(n\) is a product of two primes (erdos_700.variants.prime_mul), with \(n = 30\) a further example. The characterisation itself is open; we state it as the (unknown) set of all composite n with f n = n / P n.

This follows the largest-prime reading on erdosproblems.com. In [ErSz78, p. 98], the first prose line below (7) reads: "where \(P(n)\) is the greatest prime power which divides \(n\)." The paper's reading is stated with \(Q(n)\) in erdos_700.variants.prime_power_divisor.

theorem erdos_700.parts.i :
    {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ f n = n / P n} = erdos_700.parts.i.answer

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

Erdos700.erdos_700.variants.prime_power_divisor

Open: stated without proof.

Characterise those composite \(n\) such that \(f(n) = n/Q(n)\), where \(Q(n)\) is the largest prime-power divisor of \(n\). This is the reading of part (a) in Erdős–Szekeres ErSz78, pp. 98–99.

theorem erdos_700.variants.prime_power_divisor :
    {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ f n = n / Q n} = erdos_700.variants.prime_power_divisor.answer

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

Erdos700.erdos_700.parts.ii

Open: stated without proof.

Let \(f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})\).

(b) Are there infinitely many composite \(n\) such that \(f(n) > n^{1/2}\)?

Erdős–Szekeres [ErSz78] could not prove this. (Since \(f(n) \ge p(n)\), the least prime factor of \(n\), there are infinitely many \(n\) — those of the form \(p^2\) — with \(f(n) \ge n^{1/2}\); the question asks for the strict inequality.) Here \(f(n) > n^{1/2}\) is written as (f n) ^ 2 > n.

theorem erdos_700.parts.ii :
    {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ (f n) ^ 2 > n}.Infinite

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

Erdos700.erdos_700.parts.iii

Open: stated without proof.

Let \(f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})\).

(c) Is it true that, for every composite \(n\), \(f(n) \ll_A n/(\log n)^A\) for every \(A > 0\)?

Erdős–Szekeres [ErSz78] prove the weaker bound \(f(n) \le (1 + o(1)) n/\log n\) (the case \(A = 1\)). Here \(f(n) \ll_A n/(\log n)^A\) is spelled out as: for every A > 0 there is a constant C (depending on A) with f(n) ≤ C · n/(log n)^A for every composite n.

theorem erdos_700.parts.iii :
    (∀ A : ℝ, 0 < A → ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, ¬ n.Prime → 1 < n →
      (f n : ℝ) ≤ C * (n : ℝ) / (Real.log n) ^ A)

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

Erdos700.erdos_700.variants.prime_pow

Proved here.

f(p^a) = p for a prime p and a ≥ 2 (recorded by Erdős–Szekeres [ErSz78]). In particular, since (p^a) / P(p^a) = p^{a-1}, the prime power p^a is a "hit" (f(n) = n / P(n)) if and only if a = 2.

theorem erdos_700.variants.prime_pow (p a : ℕ) (hp : p.Prime) (ha : 2 ≤ a) : f (p ^ a) = p

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

Erdos700.erdos_700.variants.prime_mul

Proved here.

f(pq) = p for distinct primes p < q (recorded by Erdős–Szekeres [ErSz78]); in particular pq is always a "hit" (f(pq) = pq / P(pq) = p). Proof via Lucas' theorem: p ∤ C(pq,k) ⟹ p ∣ k (and the same for q), so any k with gcd(pq, C(pq,k)) = 1 must be a multiple of pq, of which there are none in (1, pq/2]; the witness k = q gives gcd(pq, C(pq,q)) = p.

theorem erdos_700.variants.prime_mul (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p < q) :
    f (p * q) = p

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

Sources

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

LeanErdos700.erdos_700.parts.i · Erdos700.erdos_700.variants.prime_power_divisor · Erdos700.erdos_700.parts.ii · Erdos700.erdos_700.parts.iii · Erdos700.erdos_700.variants.prime_pow · Erdos700.erdos_700.variants.prime_mul

TheoremErdős Problem 701#

Reference: erdosproblems.com/701

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

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

Erdos701.erdos_701

Open: stated without proof.

Let \(\mathcal{F}\) be a family of sets closed under taking subsets (i.e. if \(B\subseteq A\in\mathcal{F}\) then \(B\in \mathcal{F}\)). There exists some element \(x\) such that whenever \(\mathcal{F}'\subseteq \mathcal{F}\) is an intersecting subfamily we have

\[\lvert \mathcal{F}'\rvert \leq \lvert \{ A\in \mathcal{F} : x\in A\}\rvert.\]

theorem erdos_701 : ∀ {X : Type} [Nonempty X] [Fintype X],
    ∀ (F : Set (Set X)), IsLowerSet F →
      ∃ x : X, ∀ᵉ (F' ⊆ F),
        F'.Intersecting →
          (#F' ≤ #{ A : Set X | A ∈ F ∧ x ∈ A })

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

Sources

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

LeanErdos701.erdos_701

TheoremErdős Problem 702#

References: - erdosproblems.com/702 - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [Er76b] Erdős, P., Problems and results in graph theory and combinatorial analysis. Proceedings of the Fifth British Combinatorial Conference (Univ. Aberdeen, Aberdeen, 1975) (1976), 169-192. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Fr77] Frankl, Péter, On families of finite sets no two of which intersect in a singleton. Bull. Austral. Math. Soc. (1977), 125-134.

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

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

Erdos702.erdos_702

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

Let \(k\geq 4\). If \(\mathcal{F}\) is a family of subsets of \(\{1,\ldots,n\}\) with \(\lvert A\rvert=k\) for all \(A\in \mathcal{F}\) and \(\lvert \mathcal{F}\rvert >\binom{n-2}{k-2}\) then there are \(A,B\in\mathcal{F}\) such that \(\lvert A\cap B\rvert=1\).

A conjecture of Erdős and Sós. Katona (unpublished) proved this when \(k=4\), and Frankl [Fr77] proved this for all \(k\geq 4\).

Frankl's theorem is for \(n\) sufficiently large in terms of \(k\), and this is the form stated here. Without this assumption the statement is false, see erdos_702.variants.all_n_false.

theorem erdos_702 (k : ℕ) (hk : 4 ≤ k) :
    ∀ᶠ n in atTop, ∀ 𝓕 : Finset (Finset (Fin n)), 𝓕.IsUniform k →
      (n - 2).choose (k - 2) < 𝓕.card → ∃ A ∈ 𝓕, ∃ B ∈ 𝓕, (A ∩ B).card = 1

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

Erdos702.erdos_702.variants.all_n_false

Textbook result, proved here.

The statement does not hold for all \(n\). For \(k=4\) and \(n=5\), the family of all \(4\)-subsets of \(\{1,\ldots,5\}\) has \(5>\binom{3}{2}\) members, and any two of them meet in at least \(3\) elements.

theorem erdos_702.variants.all_n_false :
    ¬ ∀ k : ℕ, 4 ≤ k → ∀ (n : ℕ) (𝓕 : Finset (Finset (Fin n))), 𝓕.IsUniform k →
      (n - 2).choose (k - 2) < 𝓕.card → ∃ A ∈ 𝓕, ∃ B ∈ 𝓕, (A ∩ B).card = 1

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/702.lean, line 68.

Sources

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

LeanErdos702.erdos_702 · Erdos702.erdos_702.variants.all_n_false

TheoremErdős Problem 703#

References: - erdosproblems.com/703 - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [Er76b] Erdős, P., Problems and results in graph theory and combinatorial analysis. Proceedings of the Fifth British Combinatorial Conference (Univ. Aberdeen, Aberdeen, 1975) (1976), 169-192. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [FrFu84b] Frankl, P. and Füredi, Z., On hypergraphs without two edges intersecting in a given number of vertices. J. Combin. Theory Ser. A (1984), 230-236. - [Fr77b] Frankl, P., An intersection problem for finite sets. Acta Math. Acad. Sci. Hungar. (1977), 371-373. - [FrRo87] Frankl, Peter and Rödl, Vojtech, Forbidden intersections. Trans. Amer. Math. Soc. (1987), 259-286.

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

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

Erdos703.erdos_703

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

Let \(r\geq 1\) and define \(T(n,r)\) to be maximal such that there exists a family \(\mathcal{F}\) of subsets of \(\{1,\ldots,n\}\) of size \(T(n,r)\) such that \(\lvert A\cap B\rvert\neq r\) for all \(A,B\in \mathcal{F}\).

Estimate \(T(n,r)\) for \(r\geq 2\). In particular, is it true that for every \(\epsilon>0\) there exists \(\delta>0\) such that for all \(\epsilon n\lt r<(1/2-\epsilon) n\) we have

\[T(n,r)<(2-\delta)^n?\]

The answer is yes, proved by Frankl and Rödl [FrRo87].

theorem erdos_703 :
    ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      ∀ (n r : ℕ), ε * n < r → r < (1 / 2 - ε) * n → (T n r : ℝ) < (2 - δ) ^ n

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

Erdos703.erdos_703.variants.zero

Textbook result, proved here.

It is trivial that \(T(n,0)=2^{n-1}\).

theorem erdos_703.variants.zero (n : ℕ) (hn : 1 ≤ n) : T n 0 = 2 ^ (n - 1)

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/703.lean, line 76.

Erdos703.erdos_703.variants.frankl_furedi

Solved: stated here without proof.

Frankl and Füredi [FrFu84b] proved that, for fixed \(r\) and \(n\) sufficiently large in terms of \(r\), the maximal \(T(n,r)\) is achieved by taking

\[\mathcal{F} = \left\{ A\subseteq \{1,\ldots,n\} : \lvert A\rvert> \frac{n+r}{2}\textrm{ or } \lvert A\rvert < r\right\}\]

when \(n+r\) is odd, and

\[\mathcal{F} = \left\{ A\subseteq \{1,\ldots,n\} : \lvert A\backslash \{1\}\rvert\geq \frac{n+r}{2}\textrm{ or }\lvert A\rvert < r\right\}\]

when \(n+r\) is even.

theorem erdos_703.variants.frankl_furedi (r : ℕ) : ∀ᶠ n : ℕ in Filter.atTop,
    T n r = if (n + r) % 2 = 1 then
      ((univ : Finset (Finset (Fin n))).filter fun A ↦
        (n + r : ℝ) / 2 < A.card ∨ A.card < r).card
    else
      ((univ : Finset (Finset (Fin n))).filter fun A ↦
        (n + r : ℝ) / 2 ≤ (A.filter fun i : Fin n ↦ (i : ℕ) ≠ 0).card ∨
          A.card < r).card

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

Sources

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

LeanErdos703.erdos_703 · Erdos703.erdos_703.variants.zero · Erdos703.erdos_703.variants.frankl_furedi

TheoremErdős Problem 704#

References: - erdosproblems.com/704 - [Da26] Davies, J., Measurable obstructions for unmeasurable colourings. Preprint (2026). arXiv:2610.12301 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [FrWi81] Frankl, P. and Wilson, R. M., Intersection theorems with geometric consequences. Combinatorica (1981), 357-368. - [LaRo72] Larman, D. G. and Rogers, C. A., The realization of distances within sets in Euclidean space. Mathematika (1972), 1-24. - [Pr20] Prosanov, R., A new proof of the Larman-Rogers upper bound for the chromatic number of the Euclidean space. Discrete Appl. Math. (2020), 115-120. - [Ra00] Raigorodskii, A. M., On the chromatic number of a space. Uspekhi Mat. Nauk (2000), 147-148.

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

The file states 9 research or textbook statements: 1 open, 7 solved and 1 textbook result.

Erdos704.erdos_704.parts.i

Solved: stated here without proof.

Does \(\chi(G_n)\) grow exponentially in \(n\)?

Yes: Frankl and Wilson [FrWi81] proved an exponential lower bound and Larman and Rogers [LaRo72] proved an exponential upper bound. Here exponential growth means that there are constants \(1 < c \leq C\) such that \(c^n \leq \chi(G_n) \leq C^n\) for all large \(n\).

theorem erdos_704.parts.i :
    (∃ c > (1 : ℝ), ∀ᶠ n : ℕ in atTop,
      ∀ k : ℕ, (unitDistanceGraph n).Colorable k → c ^ n ≤ (k : ℝ)) ∧
    ∃ C : ℝ, ∀ᶠ n : ℕ in atTop,
      ∃ k : ℕ, (unitDistanceGraph n).Colorable k ∧ (k : ℝ) ≤ C ^ n

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 62.

Erdos704.erdos_704.parts.ii

Open: stated without proof.

Let \(G_n\) be the unit distance graph in \(\mathbb{R}^n\), with two vertices joined by an edge if and only if the distance between them is \(1\). Does

\[\lim_{n\to\infty}\chi(G_n)^{1/n}\]

exist?

This generalises the Hadwiger–Nelson problem (Erdős Problem 508), the case \(n = 2\). The chromatic number is finite (see Erdos704.erdos_704.variants.cube_colouring).

theorem erdos_704.parts.ii :
    ∃ L : ℝ, Tendsto
      (fun n : ℕ ↦ ((unitDistanceGraph n).chromaticNumber.toNat : ℝ) ^ (1 / (n : ℝ)))
      atTop (𝓝 L)

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 79.

Erdos704.erdos_704.variants.cube_colouring

Textbook result, stated without proof.

The trivial colouring (by tiling with cubes) gives

\[\chi(G_n) \leq (2 + \sqrt{n})^n.\]

In particular \(\chi(G_n)\) is finite for every \(n\).

theorem erdos_704.variants.cube_colouring :
    ∀ n : ℕ, ∃ k : ℕ, (unitDistanceGraph n).Colorable k ∧
      (k : ℝ) ≤ (2 + Real.sqrt n) ^ n

Category textbook; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 91.

Erdos704.erdos_704.variants.frankl_wilson

Solved: stated here without proof.

Frankl and Wilson [FrWi81] proved

\[\chi(G_n) \geq (1 + o(1)) 1.2^n.\]

theorem erdos_704.variants.frankl_wilson :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      ∀ k : ℕ, (unitDistanceGraph n).Colorable k → (1 - ε) * 1.2 ^ n ≤ (k : ℝ)

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 101.

Erdos704.erdos_704.variants.raigorodskii

Solved: stated here without proof.

Raigorodskii [Ra00] proved

\[\chi(G_n) \geq (1.239\cdots + o(1))^n.\]

We state the weaker bound with the truncated constant \(1.239\): for every \(0 < c < 1.239\) we have \(\chi(G_n) \geq c^n\) for all large \(n\).

theorem erdos_704.variants.raigorodskii :
    ∀ c ∈ Set.Ioo (0 : ℝ) 1.239, ∀ᶠ n : ℕ in atTop,
      ∀ k : ℕ, (unitDistanceGraph n).Colorable k → c ^ n ≤ (k : ℝ)

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 113.

Erdos704.erdos_704.variants.davies_lower

Solved: stated here without proof.

Davies [Da26, Theorem 1.4] proved

\[\chi(G_n) \geq (2 + o(1))^n,\]

improving the bound of Raigorodskii (see Erdos704.erdos_704.variants.raigorodskii): for every \(0 < c < 2\) we have \(\chi(G_n) \geq c^n\) for all large \(n\).

theorem erdos_704.variants.davies_lower :
    ∀ c ∈ Set.Ioo (0 : ℝ) 2, ∀ᶠ n : ℕ in atTop,
      ∀ k : ℕ, (unitDistanceGraph n).Colorable k → c ^ n ≤ (k : ℝ)

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 125.

Erdos704.erdos_704.variants.larman_rogers

Solved: stated here without proof.

Larman and Rogers [LaRo72] proved

\[\chi(G_n) \leq (3 + o(1))^n.\]

Prosanov [Pr20] has given an alternative proof of this bound.

theorem erdos_704.variants.larman_rogers :
    ∀ C > (3 : ℝ), ∀ᶠ n : ℕ in atTop,
      ∃ k : ℕ, (unitDistanceGraph n).Colorable k ∧ (k : ℝ) ≤ C ^ n

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 136.

Erdos704.erdos_704.variants.davies_upper

Solved: stated here without proof.

Davies [Da26, Theorem 1.5] proved

\[\chi(G_n) \leq (3\sqrt{3}/2 + o(1))^n,\]

improving the bound of Larman and Rogers (see Erdos704.erdos_704.variants.larman_rogers). (The abstract of [Da26] prints \(3\sqrt{3}/4\); Theorem 1.5 has \(3\sqrt{3}/2 \approx 2.598\).)

theorem erdos_704.variants.davies_upper :
    ∀ C > 3 * Real.sqrt 3 / 2, ∀ᶠ n : ℕ in atTop,
      ∃ k : ℕ, (unitDistanceGraph n).Colorable k ∧ (k : ℝ) ≤ C ^ n

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 148.

Erdos704.erdos_704.variants.larman_rogers_conjecture

Solved: stated here without proof.

Larman and Rogers [LaRo72] conjecture that the truth may be

\[\chi(G_n) = (2^{3/2} + o(1))^n,\]

that is, \(\chi(G_n)^{1/n} \to 2^{3/2}\).

This is false: by Erdos704.erdos_704.variants.davies_upper [Da26] we have \(\limsup \chi(G_n)^{1/n} \leq 3\sqrt{3}/2 < 2^{3/2}\). Whether the limit exists remains open (Erdos704.erdos_704.parts.ii).

theorem erdos_704.variants.larman_rogers_conjecture :
    ¬ Tendsto
      (fun n : ℕ ↦ ((unitDistanceGraph n).chromaticNumber.toNat : ℝ) ^ (1 / (n : ℝ)))
      atTop (𝓝 ((2 : ℝ) ^ ((3 : ℝ) / 2)))

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/704.lean, line 163.

Sources

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

LeanErdos704.erdos_704.parts.i · Erdos704.erdos_704.parts.ii · Erdos704.erdos_704.variants.cube_colouring · Erdos704.erdos_704.variants.frankl_wilson · Erdos704.erdos_704.variants.raigorodskii · Erdos704.erdos_704.variants.davies_lower · Erdos704.erdos_704.variants.larman_rogers · Erdos704.erdos_704.variants.davies_upper · Erdos704.erdos_704.variants.larman_rogers_conjecture

TheoremErdős Problem 705#

References: - erdosproblems.com/705 - [OD99] P. O'Donnell, High girth unit-distance graphs. PhD Dissertation, Rutgers University (1999).

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

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

Erdos705.erdos_705

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

Let \(G\) be a finite unit distance graph in \(\mamthbb{R}^2\). Is there some \(k\) such that if \(G\) has girth \(≥ k\), then \(\chi(G) ≤ 3\)?

The general case was solved by O'Donnell [OD99], who constructed finite unit distance graphs with chromatic number \(4\) and arbitrarily large girth.

theorem erdos_705:
  ¬ ∃ k, ∀ V : Set ℝ², V.Finite →
    (UnitDistancePlaneGraph V).girth ≥ k → (UnitDistancePlaneGraph V).chromaticNumber ≤ 3

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

Sources

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

LeanErdos705.erdos_705

TheoremErdős Problem 706#

References: - erdosproblems.com/706 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.

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

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

Erdos706.erdos_706

Open: stated without proof.

Let \(L(r)\) be such that if \(G\) is a graph formed by taking a finite set of points \(P\) in \(\mathbb{R}^2\) and some set \(A\subset (0,\infty)\) of size \(r\), where the vertex set is \(P\) and there is an edge between two points if and only if their distance is a member of \(A\), then \(\chi(G)\leq L(r)\).

Estimate \(L(r)\). In particular, is it true that \(L(r)\leq r^{O(1)}\)?

The case \(r=1\) is the Hadwiger-Nelson problem, for which it is known that \(5\leq L(1)\leq 7\).

See also 508, 704, and 705.

Here \(L(r)\leq r^{O(1)}\) is read as: there is \(C\) with \(\chi(G)\leq r^C\) for all large \(r\). Small \(r\) must be excluded, since \(L(1)\geq 5 > 1^C\).

theorem erdos_706 :
    ∃ C : ℕ, ∀ᶠ r : ℕ in atTop, ∀ (P : Finset ℝ²) (A : Finset ℝ), A.card = r →
      (∀ a ∈ A, 0 < a) →
      (SimpleGraph.DistancePlaneGraph (A : Set ℝ) (P : Set ℝ²)).chromaticNumber ≤
        (r ^ C : ℕ)

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/706.lean, line 54.

Sources

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

LeanErdos706.erdos_706

TheoremErdős Problem 707: Embedding Sidon Sets in Perfect Difference Sets#

References: - erdosproblems.com/707 - arxiv/2510.19804 Boris Alexeev and Dustin G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof (2025) - [Ha47] Marshall Hall, Jr., Cyclic projective planes, Duke Math. J. 14 (1947), 1079–1090.

Let A ⊆ ℕ be a finite Sidon set. Is there some set B with A ⊆ B which is a perfect difference set modulo p^2 + p + 1 for some prime power p?

This problem is related to Erdős Problem 329 about the maximum density of Sidon sets. If this conjecture is true, it would imply that the maximum density of Sidon sets is 1.

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

The file states 11 research or textbook statements: 6 solved and 5 textbook results.

Erdos707.erdos_707

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

Erdős Problem 707: It is false that any finite Sidon set can be embedded in a perfect different set modulo some \(n\).

As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.

This was formalized in Lean by Alexeev using ChatGPT.

theorem erdos_707 : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ᵉ (B : Set ℕ) (n > 0), A ⊆ B ∧ IsPerfectDifferenceSet B n) ↔ False

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

Erdos707.erdos_707.variants.prime_power

Solved: stated here without proof.

It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime power p.

As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized. -

theorem erdos_707.variants.prime_power : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧
    IsPerfectDifferenceSet B (p^2 + p + 1)) ↔ False

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

Erdos707.erdos_707.variants.prime

Solved: stated here without proof.

It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime p.

As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.

theorem erdos_707.variants.prime : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ᵉ (B : Set ℕ) (p : ℕ), p.Prime ∧ A ⊆ B ∧ IsPerfectDifferenceSet B (p^2 + p + 1)) ↔ False

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

Erdos707.erdos_707.variants.counterexample_prime

Solved: stated here without proof.

Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, proving that \(\{1,2,4,8\}\) cannot be extended to a perfect difference set modulo \(p^2+p+1\) for any prime \(p\).

theorem erdos_707.variants.counterexample_prime (A : Set ℕ) (hA : A = {1, 2, 4, 8}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (p : ℕ),
    Prime p → A ⊆ B → ¬IsPerfectDifferenceSet B (p ^ 2 + p + 1)

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

Erdos707.erdos_707.variants.counterexample_mian_chowla

Solved: stated here without proof.

Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, showing that \(\{1, 2, 4, 8, 13\}\) cannot be extended to any perfect difference set modulo a positive integer. The modulus 0 is excluded, as in erdos_707: IsPerfectDifferenceSet B 0 describes an infinite perfect difference set in ℤ, and every finite Sidon set extends to one.

theorem erdos_707.variants.counterexample_mian_chowla (A : Set ℕ) (hA : A = {1, 2, 4, 8, 13}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (n : ℕ), 0 < n → A ⊆ B → ¬IsPerfectDifferenceSet B n

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

Erdos707.erdos_707.variants.counterexample_hall

Solved: stated here without proof.

This conjecture was actually first disproved by Hall in 1947 [Ha47], long before Erdős asked this question. A counterexample for any modulus from from [Ha47] in the paragraph following Theorem 4.3, where it was given as \(\{-8, -6, 0, 1, 4\}\), but this can be shifted to natural numbers as pointed out in [arxiv/2510.19804].

theorem erdos_707.variants.counterexample_hall (A : Set ℕ) (hA : A = {1, 3, 9, 10, 13}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (n : ℕ), 0 < n → A ⊆ B → ¬IsPerfectDifferenceSet B n

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

Erdos707.erdos_707.variants.perfect_difference_set_size_bound

Textbook result, proved here.

A perfect difference set modulo n must have size ≤ √n + 1.

theorem erdos_707.variants.perfect_difference_set_size_bound (B : Set ℕ) (n : ℕ)
    (hB : IsPerfectDifferenceSet B n) : B.ncard ≤ n.sqrt + 1

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

Erdos707.erdos_707.variants.singer_construction

Textbook result, stated without proof.

The Singer construction gives perfect difference sets for n = p^2 + p + 1 where p is a prime power.

theorem erdos_707.variants.singer_construction (p : ℕ) (hp : IsPrimePow p) :
    ∃ (B : Set ℕ), IsPerfectDifferenceSet B (p^2 + p + 1) ∧ B.ncard = p + 1

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

Erdos707.erdos_707.variants.example_sidon_set

Textbook result, proved here.

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

theorem erdos_707.variants.example_sidon_set : IsSidon ({1, 2, 4} : Set ℕ)

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

Erdos707.erdos_707.variants.example_embedding

Textbook result, proved here.

The set {1, 2, 4} can be embedded in a perfect difference set modulo 7.

theorem erdos_707.variants.example_embedding : ∃ (B : Set ℕ), {1, 2, 4} ⊆ B ∧
    IsPerfectDifferenceSet B 7

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

Erdos707.erdos_707.variants.small_sidon_sets

Textbook result, stated without proof.

For small Sidon sets, we can check the conjecture directly.

theorem erdos_707.variants.small_sidon_sets (A : Set ℕ) (hA : A.Finite) (h : A.ncard ≤ 3)
    (hSidon : IsSidon A) : ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧
    IsPerfectDifferenceSet B (p^2 + p + 1)

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

Sources

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

LeanErdos707.erdos_707 · Erdos707.erdos_707.variants.prime_power · Erdos707.erdos_707.variants.prime · Erdos707.erdos_707.variants.counterexample_prime · Erdos707.erdos_707.variants.counterexample_mian_chowla · Erdos707.erdos_707.variants.counterexample_hall · Erdos707.erdos_707.variants.perfect_difference_set_size_bound · Erdos707.erdos_707.variants.singer_construction · Erdos707.erdos_707.variants.example_sidon_set · Erdos707.erdos_707.variants.example_embedding · Erdos707.erdos_707.variants.small_sidon_sets

TheoremErdős Problem 709#

References: - erdosproblems.com/709 - [ErSu59] P. Erdős and J. Surányi, Bemerkungen zu einer Aufgabe eines mathematischen Wettbewerbs, Mat. Lapok 10 (1959), 39–48. - [Er92c] P. Erdős, Some of my forgotten problems in number theory, Hardy–Ramanujan J. 15 (1992), 34–50. - [vD26] W. van Doorn, On the length of an interval that contains distinct multiples of the first \(n\) positive integers, Integers (2026), #A7.

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

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

Erdos709.erdos_709.variants.singleton

Textbook result, proved here.

Erdős Problem 709 holds for a singleton input: the multiplier 1 suffices.

theorem erdos_709.variants.singleton : Works 1 1

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

Erdos709.erdos_709

Open: stated without proof.

Let \(f(n)\) be minimal such that, for any \(A=\{a_1,\ldots,a_n\}\subseteq [2,\infty)\cap\mathbb{N}\) of size \(n\), in any interval \(I\) of \(f(n)\max(A)\) consecutive integers there exist distinct \(x_1,\ldots,x_n\in I\) such that \(a_i\mid x_i\).

Obtain good bounds for \(f(n)\), or even an asymptotic formula.

We read "good bounds" as determining the order of magnitude of \(f(n)\).

theorem erdos_709 : f =Θ[atTop] erdos_709.answer

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

Erdos709.erdos_709.variants.ersu_lower

Solved: stated here without proof.

A problem of Erdős and Surányi [ErSu59], who proved

\[(\log n)^c \ll f(n) \ll n^{1/2}\]

for some constant \(c>0\).

This is the lower bound.

theorem erdos_709.variants.ersu_lower :
    ∃ c > (0 : ℝ), (fun n : ℕ ↦ Real.log n ^ c) =O[atTop] f

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

Erdos709.erdos_709.variants.ersu_upper

Solved: stated here without proof.

A problem of Erdős and Surányi [ErSu59], who proved

\[(\log n)^c \ll f(n) \ll n^{1/2}\]

for some constant \(c>0\).

This is the upper bound.

theorem erdos_709.variants.ersu_upper :
    f =O[atTop] fun n : ℕ ↦ (n : ℝ) ^ (1 / 2 : ℝ)

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

Erdos709.erdos_709.variants.van_doorn_lower

Solved: stated here without proof.

The lower bound here can be improved, using van Doorn's lower bound for [711] from [vD26], to

\[\frac{\log n}{\log\log n}\ll f(n).\]

theorem erdos_709.variants.van_doorn_lower :
    (fun n : ℕ ↦ Real.log n / Real.log (Real.log n)) =O[atTop] f

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

Sources

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

LeanErdos709.erdos_709.variants.singleton · Erdos709.erdos_709 · Erdos709.erdos_709.variants.ersu_lower · Erdos709.erdos_709.variants.ersu_upper · Erdos709.erdos_709.variants.van_doorn_lower

TheoremErdős Problem 710#

References: - erdosproblems.com/710 - [ErPo80] Erdős, P. and Pomerance, C., Matching the natural numbers up to \(n\) with distinct multiples in another interval. Nederl. Akad. Wetensch. Indag. Math. 42 (1980), 147-161. PDF

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

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

Erdos710.erdos_710

Open: stated without proof.

Let \(f(n)\) be minimal such that in \((n,n+f(n))\) there exist distinct integers \(a_1,\ldots,a_n\) such that \(k\mid a_k\) for all \(1\leq k\leq n\). Obtain an asymptotic formula for \(f(n)\).

theorem erdos_710 : (fun n ↦ (f n : ℝ)) ~[atTop] erdos_710.answer

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

Erdos710.erdos_710.variants.lower_bound

Solved: stated here without proof.

Erdős and Pomerance [ErPo80] proved

\[\left(\frac{2}{\sqrt{e}}+o(1)\right)n\left(\frac{\log n}{\log\log n}\right)^{1/2} \leq f(n) \leq (1.7398\cdots+o(1))n(\log n)^{1/2}.\]

This is the lower bound [ErPo80, Theorem 2].

theorem erdos_710.variants.lower_bound :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (2 / Real.sqrt (Real.exp 1) - ε) * n *
        Real.sqrt (Real.log n / Real.log (Real.log n)) ≤ (f n : ℝ)

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

Erdos710.erdos_710.variants.upper_bound

Solved: stated here without proof.

Erdős and Pomerance [ErPo80] proved

\[\left(\frac{2}{\sqrt{e}}+o(1)\right)n\left(\frac{\log n}{\log\log n}\right)^{1/2} \leq f(n) \leq (1.7398\cdots+o(1))n(\log n)^{1/2}.\]

This is the upper bound. Here \(1.7398\cdots = \sqrt{r}/(1-r)\), where \(r\) is the solution of \(e^{-r} = r\) [ErPo80, (11), p. 154].

theorem erdos_710.variants.upper_bound :
    ∃ r : ℝ, Real.exp (-r) = r ∧ ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (f n : ℝ) ≤ (Real.sqrt r / (1 - r) + ε) * n * Real.sqrt (Real.log n)

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

Sources

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

LeanErdos710.erdos_710 · Erdos710.erdos_710.variants.lower_bound · Erdos710.erdos_710.variants.upper_bound

TheoremErdős Problem 711#

References: - erdosproblems.com/711 - [ErPo80] Erdős, P. and Pomerance, C., Matching the natural numbers up to \(n\) with distinct multiples in another interval (1980). - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34–50. - [vD26] van Doorn, W., On the length of an interval that contains distinct multiples of the first \(n\) positive integers. Integers 26 (2026), #A7.

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

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

Erdos711.erdos_711.parts.i

Open: stated without proof.

Let \(f(n,m)\) be minimal such that \((m,m+f(n,m))\) contains distinct integers \(a_1,\ldots,a_n\) with \(k \mid a_k\) for \(1 \leq k \leq n\). Prove that \(\max_m f(n,m) \leq n^{1+o(1)}\).

theorem erdos_711.parts.i : ∃ error : ℕ → ℝ,
    error =o[atTop] (fun _ ↦ (1 : ℝ)) ∧ ∀ᶠ n in atTop, ∀ m, ∃ L,
      HasDivisibleDistinctTuple n m L ∧ (L : ℝ) ≤ Real.rpow n (1 + error n)

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

Erdos711.erdos_711.parts.ii

Solved: stated here without proof.

Prove that \(\max_m (f(n,m)-f(n,n)) \to \infty\).

This was proved by van Doorn [vD26], who obtained the stronger lower bound \(f(n,m)-f(n,n) \gg n\log n/\log\log n\) for a suitable \(m=m(n)\) and all large \(n\).

theorem erdos_711.parts.ii : ∀ B : ℕ, ∀ᶠ n in atTop,
    ∃ m Lm Ln : ℕ, IsMinimalIntervalLength n m Lm ∧
      IsMinimalIntervalLength n n Ln ∧ B ≤ Lm - Ln

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

Sources

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

LeanErdos711.erdos_711.parts.i · Erdos711.erdos_711.parts.ii

TheoremErdős Problem 712#

References: - erdosproblems.com/712 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.

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

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

Erdos712.erdos_712

Open: stated without proof.

Determine, for any \(k>r>2\), the limiting value as \(n\to\infty\) of

\[\frac{\mathrm{ex}_r(n,K_k^r)}{\binom{n}{r}},\]

where \(\mathrm{ex}_r(n,K_k^r)\) is the largest number of \(r\)-edges which can placed on \(n\) vertices so that there exists no set of \(k\) vertices which is covered by all \(\binom{k}{r}\) possible \(r\)-edges.

theorem erdos_712 :
    ∀ k r : ℕ, 2 < r → r < k →
      Tendsto (fun n ↦ (Hypergraph.cliqueExtremalNumber n r k : ℝ) / n.choose r)
        atTop (𝓝 (erdos_712.answer k r))

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

Erdos712.erdos_712.variants.limit_exists

Textbook result, stated without proof.

The normalized extremal numbers have a limit in \([0,1]\). This existence result does not determine the value asked for in Erdős Problem 712.

theorem erdos_712.variants.limit_exists (r k : ℕ) :
    ∃ π ∈ Set.Icc (0 : ℝ) 1,
      Tendsto (fun n : ℕ ↦ (Hypergraph.cliqueExtremalNumber n r k : ℝ) / n.choose r)
        atTop (𝓝 π)

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/712.lean, line 56.

Erdos712.erdos_712.variants.graph_case

Solved: stated here without proof.

Turán's theorem gives the graph case: \(\mathrm{ex}_2(n,K_k)/\binom{n}{2}\to 1-1/(k-1)\).

theorem erdos_712.variants.graph_case (k : ℕ) (hk : 2 ≤ k) :
    Tendsto (fun n : ℕ ↦ (Hypergraph.cliqueExtremalNumber n 2 k : ℝ) / n.choose 2)
      atTop (𝓝 (1 - 1 / ((k : ℝ) - 1)))

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

Erdos712.erdos_712.variants.graph_case_div_sq

Solved: stated here without proof.

With denominator \(n^2\), Turán's graph limit is \(\frac12(1-1/(k-1))\). The factor \(\frac12\) comes from the normalization.

theorem erdos_712.variants.graph_case_div_sq (k : ℕ) (hk : 2 ≤ k) :
    Tendsto (fun n : ℕ ↦ (Hypergraph.cliqueExtremalNumber n 2 k : ℝ) / (n : ℝ) ^ 2)
      atTop (𝓝 ((1 / 2) * (1 - 1 / ((k : ℝ) - 1))))

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

Sources

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

LeanErdos712.erdos_712 · Erdos712.erdos_712.variants.limit_exists · Erdos712.erdos_712.variants.graph_case · Erdos712.erdos_712.variants.graph_case_div_sq

TheoremErdős Problem 713#

References: - erdosproblems.com/713 - [Er67d] Erdős, P., Some recent results on extremal problems in graph theory. {R}esults. (1967), 117--123 (English); pp. 124--130 (French). - [ErSi70] Erdős, P. and Simonovits, M., Some extremal problems in graph theory. Combinatorial theory and its applications, I-III (Proc. Colloq., Balatonfüred, 1969) (1970), 377-390. - [FrFu87] Frankl, P. and Füredi, Z., Exact solution of some Turán-type problems. J. Combin. Theory Ser. A (1987), 226--262. - [FuGe21] Füredi, Zoltán and Gerbner, Dániel, Hypergraphs without exponents. J. Combin. Theory Ser. A (2021), Paper No. 105517, 9.

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

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

Erdos713.erdos_713.parts.i

Open: stated without proof.

Is it true that, for every bipartite graph \(G\), there exists some \(\alpha\in [1,2)\) and \(c>0\) such that

\[\mathrm{ex}(n;G)\sim cn^\alpha?\]

The condition that \(G\) have at least two edges excludes degenerate forbidden graphs whose extremal number is eventually zero, for which the displayed asymptotic with \(c>0\) is impossible.

theorem erdos_713.parts.i :
    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
      ∃ α c : ℝ, α ∈ Set.Ico 1 2 ∧ 0 < c ∧
        Asymptotics.IsEquivalent atTop
          (fun n : ℕ => (extremalNumber n G : ℝ))
          (fun n : ℕ => c * (n : ℝ) ^ α)

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

Erdos713.erdos_713.parts.ii

Open: stated without proof.

Must \(\alpha\) be rational?

The same nondegeneracy condition on \(G\) is used as in part (i). Rationality means that the real number \(\alpha\) lies in the image of the canonical embedding \(\mathbb{Q}\to\mathbb{R}\).

theorem erdos_713.parts.ii :
    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
      ∀ α c : ℝ, α ∈ Set.Ico 1 2 → 0 < c →
        Asymptotics.IsEquivalent atTop
          (fun n : ℕ => (extremalNumber n G : ℝ))
          (fun n : ℕ => c * (n : ℝ) ^ α) →
        α ∈ Set.range ((↑) : ℚ → ℝ)

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

Sources

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

LeanErdos713.erdos_713.parts.i · Erdos713.erdos_713.parts.ii

TheoremErdős Problem 714#

References: - erdosproblems.com/714 - [Br66] Brown, W. G., On graphs that do not contain a Thomsen graph. Canad. Math. Bull. (1966), 281-285. - [ERS66] Erdős, P. and Rényi, A. and Sós, V. T., On a problem of graph theory. Studia Sci. Math. Hungar. (1966), 215--235. - [KST54] Kövari, T. and Sós, V. T. and Turán, P., On a problem of K. Zarankiewicz. Colloq. Math. (1954), 50-57.

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

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

Erdos714.erdos_714

Open: stated without proof.

Is it true that

\[\mathrm{ex}(n; K_{r,r}) \gg n^{2-1/r}?\]

theorem erdos_714 :
    ∀ r : ℕ, 2 ≤ r → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
      c * (n : ℝ) ^ ((2 : ℝ) - 1 / (r : ℝ)) ≤
        (extremalNumber n (completeBipartiteGraph (Fin r) (Fin r)) : ℝ)

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

Sources

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

LeanErdos714.erdos_714

TheoremErdős Problem 716#

References: - erdosproblems.com/716 - [BES73] Brown, W. G. and Erdős, P. and S\'os, V. T., Some extremal problems on {\(r\)}-graphs. (1973), 53--63. - [RuSz78] Ruzsa, I. Z. and Szemer\'{e}di, E., Triple systems with no six points carrying three triangles. Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Vol. II (1978), 939-945.

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

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

Erdos716.erdos_716

Solved: stated here without proof.

Let \(\mathcal{F}\) be the family of all \(3\)-uniform hypergraphs with \(6\) vertices and \(3\) \(3\)-edges. Is it true that

\[\mathrm{ex}_3(n,\mathcal{F})=o(n^2)?\]

The answer is yes, proved by Ruzsa and Szemerédi [RuSz78] (this is known as the Ruzsa-Szemerédi problem).

theorem erdos_716 :
    (fun n ↦ (Hypergraph.configurationExtremalNumber n 3 6 3 : ℝ)) =o[atTop]
      (fun n ↦ (n : ℝ) ^ 2)

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

Sources

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

LeanErdos716.erdos_716

TheoremErdős Problem 717#

References: - erdosproblems.com/717 - [ErFa81] Erdős, Paul and Fajtlowicz, Siemion, On the conjecture of Hajós. Combinatorica 1 (1981), 141-143. PDF - [FLS13] Fox, Jacob and Lee, Choongbum and Sudakov, Benny, Chromatic number, clique subdivisions, and the conjectures of Hajós and Erdős-Fajtlowicz. Combinatorica 33 (2013), 181-197. arXiv:1107.1920

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

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

Erdos717.erdos_717

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

Let \(G\) be a graph on \(n\) vertices with chromatic number \(\chi(G)\) and let \(\sigma(G)\) be the maximal \(k\) such that \(G\) contains a subdivision of \(K_k\). Is it true that

\[\chi(G) \ll \frac{n^{1/2}}{\log n}\sigma(G)?\]

The answer is yes, proved by Fox, Lee, and Sudakov [FLS13, Theorem 1.1]. We read \(\ll\) as: there is an absolute constant \(C > 0\) with this inequality for all graphs on \(n \geq 2\) vertices (for \(n = 1\), \(\log n = 0\)).

theorem erdos_717 :
    ∃ C : ℝ, 0 < C ∧
      ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
        2 ≤ Fintype.card V →
        (G.chromaticNumber.toNat : ℝ) ≤
          C * (Real.sqrt (Fintype.card V : ℝ) / Real.log (Fintype.card V : ℝ)) *
            (cliqueSubdivisionNumber G : ℝ)

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

Erdos717.erdos_717.variants.erdos_fajtlowicz

Solved: stated here without proof.

Erdős and Fajtlowicz [ErFa81, Theorem 3] showed that for almost all graphs on \(n\) vertices

\[\chi(G) \gg \frac{n^{1/2}}{\log n}\sigma(G).\]

As in [ErFa81, p. 141], "almost all" means all but \(o(2^{\binom{n}{2}})\) labelled graphs on \(n\) vertices.

theorem erdos_717.variants.erdos_fajtlowicz :
    ∃ C : ℝ, 0 < C ∧
      Tendsto (fun n : ℕ =>
        (Nat.card {G : SimpleGraph (Fin n) //
          ¬ (C * (Real.sqrt n / Real.log n) * (cliqueSubdivisionNumber G : ℝ) <
            (G.chromaticNumber.toNat : ℝ))} : ℝ) / 2 ^ n.choose 2) atTop (𝓝 0)

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

Sources

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

LeanErdos717.erdos_717 · Erdos717.erdos_717.variants.erdos_fajtlowicz

TheoremErdős Problem 719#

References: - erdosproblems.com/719

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

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

Erdos719.erdos_719

Open: stated without proof.

Let \(r\geq 2\), and let \(\mathrm{ex}_r(n;K_{r+1}^r)\) be the maximum number of \(r\)-edges that can be placed on \(n\) vertices without forming a \(K_{r+1}^r\) (the \(r\)-uniform complete graph on \(r+1\) vertices). Is every \(r\)-hypergraph \(G\) on \(n\) vertices the union of at most \(\mathrm{ex}_{r}(n;K_{r+1}^r)\) many copies of \(K_r^r\) and \(K_{r+1}^r\), no two of which share a \(K_r^r\)?

theorem erdos_719 :
    ∀ r : ℕ, 2 ≤ r → ∀ (n : ℕ) (H : Finset (Finset (Fin n))),
    H.IsUniform r → ∃ D : Finset (Finset (Fin n)),
      H.IsCompleteHypergraphDecomposition r D ∧
        D.card ≤ Hypergraph.cliqueExtremalNumber n r (r + 1)

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

Sources

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

LeanErdos719.erdos_719

TheoremErdős Problem 720#

References: - erdosproblems.com/720 - [Er76c] Erdős, P., Some recent problems and results in graph theory, combinatorics and number theory. Proceedings of the Seventh Southeastern Conference on Combinatorics, Graph Theory, and Computing (Louisiana State Univ., Baton Rouge, La., 1976) (1976), 3-14. - [EFRS78b] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., The size Ramsey number. Period. Math. Hungar. (1978), 145-161. - [Er78] Erdős, Paul, Problems and results in combinatorial analysis and combinatorial number theory. Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1978) (1978), 29-40. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Be83b] Beck, József, On size Ramsey number of paths, trees, and circuits. I. J. Graph Theory (1983), 115-129.

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

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

Erdos720.erdos_720.parts.i

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

Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges such that in any \(2\)-colouring of the edges of \(H\) there is a monochromatic copy of \(G\).

Is it true that, if \(P_n\) is the path of length \(n\), then \(\hat{R}(P_n)/n\to \infty\)?

The answer is no: Beck [Be83b] proved that in fact \(\hat{R}(P_n)\ll n\).

theorem erdos_720.parts.i :
    ¬ Tendsto (fun n : ℕ ↦ (sizeRamseyNumber (pathGraph (n + 1)) : ℝ) / n) atTop atTop

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

Erdos720.erdos_720.parts.ii

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

Is it true that, if \(P_n\) is the path of length \(n\), then \(\hat{R}(P_n)/n^2 \to 0\)?

The answer is yes: Beck [Be83b] proved that in fact \(\hat{R}(P_n)\ll n\).

theorem erdos_720.parts.ii :
    Tendsto (fun n : ℕ ↦ (sizeRamseyNumber (pathGraph (n + 1)) : ℝ) / (n : ℝ) ^ 2) atTop
      (nhds 0)

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

Erdos720.erdos_720.parts.iii

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

Is it true that, if \(C_n\) is the cycle with \(n\) edges, then \(\hat{R}(C_n) =o(n^2)\)?

The answer is yes: Beck [Be83b] proved that in fact \(\hat{R}(C_n)\ll n\).

theorem erdos_720.parts.iii :
    Tendsto (fun n : ℕ ↦ (sizeRamseyNumber (cycleGraph n) : ℝ) / (n : ℝ) ^ 2) atTop
      (nhds 0)

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

Erdos720.erdos_720.variants.beck

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

Beck [Be83b] proved that \(\hat{R}(P_n)\ll n\) and \(\hat{R}(C_n)\ll n\).

theorem erdos_720.variants.beck :
    ∃ C : ℕ, ∀ᶠ n : ℕ in atTop,
      sizeRamseyNumber (pathGraph (n + 1)) ≤ C * n ∧
        sizeRamseyNumber (cycleGraph n) ≤ C * n

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

Sources

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

LeanErdos720.erdos_720.parts.i · Erdos720.erdos_720.parts.ii · Erdos720.erdos_720.parts.iii · Erdos720.erdos_720.variants.beck

TheoremErdős Problem 721#

References: - erdosproblems.com/721 - [Gr22] Green, B., New lower bounds for van der Waerden numbers. arXiv:2102.01543. - [Hu22] Hunter, Z., Improved lower bounds for van der Waerden numbers. arXiv:2111.01099. - [Sc21] Schoen, T., A subexponential upper bound for van der Waerden numbers W(3,k). arXiv:2006.02877.

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

The file states 2 research or textbook statements: 2 solved. It also has 2 API statements, counted here but not shown.

Erdos721.erdos_721.upper_bound

Solved: stated here without proof.

Erdős Problem 721, upper bound: prove that \(W(3,k) < \exp(k^c)\) for some constant \(c<1\).

The first to show that \(W(3,k) < \exp(k^c)\) for some \(c<1\) was Schoen [Sc21]. Source: erdosproblems.com/721. The exponent is fixed independently of \(k\), and the bound holds for all sufficiently large \(k\).

theorem erdos_721.upper_bound : SubexponentialUpperBound

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

Erdos721.erdos_721.lower_bound

Solved: stated here without proof.

Erdős Problem 721, lower bound: Hunter [Hu22] improved this to \(W(3,k) \geq \exp\left(c\frac{(\log k)^2}{\log\log k}\right)\) for some constant \(c>0\).

Source: erdosproblems.com/721. This eventual bound uses a nonforcing interval of length \(N\) and the successor \(N+1\) as a lower bound for the least forcing integer.

theorem erdos_721.lower_bound : HunterLowerBound

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

Sources

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

LeanErdos721.erdos_721.upper_bound · Erdos721.erdos_721.lower_bound

TheoremErdős Problem 722#

References: - erdosproblems.com/722 - [Ha61] Hanani, Haim, The existence and construction of balanced incomplete block designs. Ann. Math. Statist. (1961), 361-386. - [Ke14] P. Keevash, The existence of designs. arXiv:1401.3665 (2014). - [Wi72] Wilson, Richard M., An existence theory for pairwise balanced designs. {II}. The structure of {PBD}-closed sets and the existence conjectures. J. Combinatorial Theory Ser. A (1972), 246-273.

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

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

Erdos722.erdos_722

Solved: stated here without proof.

Let \(k>r\) and \(n\) be sufficiently large in terms of \(k\) and \(r\). Does there always exist a block \(r-(n,k,1)\) design (or Steiner system with parameters \((n,k,r)\)), provided the trivial necessary divisibility conditions \(\binom{k-i}{r-i}\mid \binom{n-i}{r-i}\) are satisfied for every \(0\leq i\lt r\)? That is, can one find a family of \(\binom{n}{r}\binom{k}{r}^{-1}\) many subsets of \(\{1,\ldots,n\}\), all of size \(k\), such that any \(A\subseteq \{1,\ldots,n\}\) of size \(r\) is contained in exactly one set in the family?

This was proved by Keevash [Ke14] for all \((r,k)\).

theorem erdos_722 :
    ∀ r k : ℕ, 1 ≤ r → r < k → ∀ᶠ n : ℕ in atTop,
    (∀ i < r, (k - i).choose (r - i) ∣ (n - i).choose (r - i)) →
      ∃ H : Finset (Finset (Fin n)), H.IsBlockDesign r k

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

Sources

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

LeanErdos722.erdos_722

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.