Erdős Problem 723: The prime… to Erdős Problem 747
TheoremErdős Problem 723: The prime power conjecture.#
Reference: erdosproblems.com/723
Quoted from FormalConjectures/ErdosProblems/723.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/723.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos723.erdos_723
Open: stated without proof.
If there is a finite projective plane of order \(n\) then must \(n\) be a prime power?
theorem erdos_723 :
∀ {P L : Type} (_: Membership P L) (_ : Fintype P) (_ : Fintype L),
∀ pp : ProjectivePlane P L, IsPrimePow pp.order
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/723.lean, line 36.
Erdos723.erdos_723.variants.prime_power_is_projplane_order
Solved: stated here without proof.
These always exist if \(n\) is a prime power.
theorem erdos_723.variants.prime_power_is_projplane_order :
∀ n, IsPrimePow n → ∃ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L)
(pp : ProjectivePlane P L), pp.order = n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/723.lean, line 45.
Erdos723.erdos_723.variants.leq_11
Solved: stated here without proof.
This conjecture has been proved for \(n \leq 11\).
theorem erdos_723.variants.leq_11 {P L : Type} [Membership P L] [Fintype P] [Fintype L] :
∀ pp : ProjectivePlane P L, pp.order ≤ 11 → IsPrimePow pp.order
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/723.lean, line 54.
Erdos723.erdos_723.variants.eq_12
Open: stated without proof.
It is open whether there exists a projective plane of order 12.
theorem erdos_723.variants.eq_12 :
∃ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L) (pp : ProjectivePlane P L),
pp.order = 12
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/723.lean, line 62.
Erdos723.erdos_723.variants.bruck_ryser
Solved: stated here without proof.
Bruck and Ryser have proved that if \(n \equiv 1 (\mod 4)\) or \(n \equiv 2 (\mod 4)\) then \(n\) must be the sum of two squares.
theorem erdos_723.variants.bruck_ryser {P L : Type} [Membership P L] [Fintype P] [Fintype L]
(n : ℕ) (pp : ProjectivePlane P L) (hpp : pp.order = n) :
(n ≡ 1 [MOD 4] ∨ n ≡ 2 [MOD 4]) → ∃ a b, n = a ^ 2 + b ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/723.lean, line 72.
Sources
TheoremErdős Problem 724#
References: - erdosproblems.com/724 - OEIS A001438 - [Be83c] Beth, Thomas, Eine Bemerkung zur Abschätzung der Anzahl orthogonaler lateinischer Quadrate mittels Siebverfahren. Abh. Math. Sem. Univ. Hamburg (1983), 284-288. - [BPS60] Bose, R. C. and Shrikhande, S. S. and Parker, E. T., Further results on the construction of mutually orthogonal Latin squares and the falsity of Euler's conjecture. Canadian J. Math. (1960), 189-203. - [CES60] Chowla, S. and Erdős, P. and Straus, E. G., On the maximal number of pairwise orthogonal Latin squares of a given order. Canadian J. Math. (1960), 204-208. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Wi74] Wilson, Richard M., Concerning the number of mutually orthogonal Latin squares. Discrete Math. (1974), 181-198.
Quoted from FormalConjectures/ErdosProblems/724.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/724.
The file states 7 research or textbook statements: 1 open, 5 solved and 1 textbook result.
Erdos724.erdos_724
Open: stated without proof.
Let \(f(n)\) be the maximum number of mutually orthogonal Latin squares of order \(n\). Is it true that
\[f(n) \gg n^{1/2}?\]This question is from [Er81].
theorem erdos_724 :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, c * Real.sqrt (n : ℝ) ≤ (maxMOLS n : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 69.
Erdos724.erdos_724.variants.euler_conjecture
Solved: stated here without proof.
Euler conjectured that \(f(n) = 1\) when \(n \equiv 2 \pmod{4}\). This is false: Bose, Parker, and Shrikhande [BPS60] proved \(f(n) \geq 2\) for \(n \geq 7\), so for example \(f(10) \geq 2\).
theorem erdos_724.variants.euler_conjecture :
¬ ∀ n : ℕ, n ≡ 2 [MOD 4] → maxMOLS n = 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 78.
Erdos724.erdos_724.variants.bose_parker_shrikhande
Solved: stated here without proof.
Bose, Parker, and Shrikhande [BPS60] proved that \(f(n) \geq 2\) for all \(n \geq 7\).
theorem erdos_724.variants.bose_parker_shrikhande :
∀ n : ℕ, 7 ≤ n → 2 ≤ maxMOLS n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 86.
Erdos724.erdos_724.variants.chowla_erdos_straus
Solved: stated here without proof.
Chowla, Erdős, and Straus [CES60] proved that
\[f(n) \gg n^{1/91}.\]
theorem erdos_724.variants.chowla_erdos_straus :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
c * (n : ℝ) ^ ((1 : ℝ) / 91) ≤ (maxMOLS n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 95.
Erdos724.erdos_724.variants.wilson
Solved: stated here without proof.
Wilson [Wi74] proved that
\[f(n) \gg n^{1/17}.\]
theorem erdos_724.variants.wilson :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
c * (n : ℝ) ^ ((1 : ℝ) / 17) ≤ (maxMOLS n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 105.
Erdos724.erdos_724.variants.beth
Solved: stated here without proof.
Beth [Be83c] proved that
\[f(n) \gg n^{1/14.8}.\]
theorem erdos_724.variants.beth :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
c * (n : ℝ) ^ ((1 : ℝ) / 14.8) ≤ (maxMOLS n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 115.
Erdos724.erdos_724.variants.le_sub_one
Textbook result, proved here.
For \(n \geq 2\) there are at most \(n - 1\) mutually orthogonal Latin squares of order \(n\):
\[f(n) \leq n - 1.\]This is classical; see OEIS A001438.
theorem erdos_724.variants.le_sub_one :
∀ n : ℕ, 2 ≤ n → maxMOLS n ≤ n - 1
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/724.lean, line 126.
Sources
TheoremErdős Problem 725#
References: - erdosproblems.com/725 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica 1 (1981), 25-42. PDF - [ErKa46] Erdős, P. and Kaplansky, I., The asymptotic number of Latin rectangles. Amer. J. Math. 68 (1946), 230-236. PDF - [Ya51] Yamamoto, K., On the asymptotic number of Latin rectangles. Jpn. J. Math. 21 (1951), 113-119.
Quoted from FormalConjectures/ErdosProblems/725.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/725.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos725.erdos_725
Open: stated without proof.
Give an asymptotic formula for the number of \(k\times n\) Latin rectangles.
The formula \(F(k,n)\) must satisfy \(L(k,n)\sim F(k,n)\) as \(n\to\infty\) for every choice of \(k=k(n)\leq n\), so it also covers Latin squares (\(k=n\)).
theorem erdos_725 (k : ℕ → ℕ) (hk : ∀ n, k n ≤ n) :
(fun n ↦ (L (k n) n : ℝ)) ~[atTop] fun n ↦ erdos_725.answer (k n) n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/725.lean, line 74.
Erdos725.erdos_725.variants.erdos_kaplansky
Solved: stated here without proof.
Erdős and Kaplansky [ErKa46] proved the count is
\[\sim e^{-\binom{k}{2}}(n!)^k\]when \(k=o((\log n)^{3/2-\epsilon})\).
Here \(\epsilon>0\) is fixed.
theorem erdos_725.variants.erdos_kaplansky (ε : ℝ) (hε : 0 < ε) (k : ℕ → ℕ)
(hk : (fun n ↦ (k n : ℝ)) =o[atTop] fun n ↦ Real.log n ^ (3 / 2 - ε)) :
(fun n ↦ (L (k n) n : ℝ)) ~[atTop]
fun n ↦ Real.exp (-((k n).choose 2 : ℝ)) * (n.factorial : ℝ) ^ k n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/725.lean, line 86.
Erdos725.erdos_725.variants.yamamoto
Solved: stated here without proof.
Yamamoto [Ya51] extended this to \(k\leq n^{1/3-o(1)}\).
As in [Ya51, p. 113], we assume \(k\lt n^{1/3-\delta}\) with \(n^{-\delta}\to 0\), where \(\delta\) may be a positive constant or a function of \(n\).
theorem erdos_725.variants.yamamoto (δ : ℕ → ℝ)
(hδ : Tendsto (fun n : ℕ ↦ (n : ℝ) ^ (-δ n)) atTop (nhds 0)) (k : ℕ → ℕ)
(hk : ∀ᶠ n in atTop, (k n : ℝ) < (n : ℝ) ^ (1 / 3 - δ n)) :
(fun n ↦ (L (k n) n : ℝ)) ~[atTop]
fun n ↦ Real.exp (-((k n).choose 2 : ℝ)) * (n.factorial : ℝ) ^ k n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/725.lean, line 99.
Sources
TheoremErdős Problem 726#
References: - erdosproblems.com/726 - [EGRS75] Erdős, P., and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \((\sp{2n}\sb{n})\). Math. Comp. (1975), 83-92.
Quoted from FormalConjectures/ErdosProblems/726.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/726.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos726.erdos_726
Open: stated without proof.
As \(n\to \infty\) ranges over integers \(\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}\)?
A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75].
By \(n\in (p/2,p)\pmod{p}\) we mean \(n\equiv r\pmod{p}\) for some integer \(r\) with \(p/2\lt r\lt p\). The remainder
n % pis computed inℕbefore casting toℝ.
theorem erdos_726 :
(fun n : ℕ ↦ ∑ p ∈ (range (n + 1)).filter
(fun p : ℕ ↦ p.Prime ∧ (p : ℝ) / 2 < ((n % p : ℕ) : ℝ)),
(1 : ℝ) / (p : ℝ))
~[atTop] (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)) / 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/726.lean, line 46.
Erdos726.erdos_726.variants.mertens_estimate
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/74888affffcf320d798f78a2fb45d13c86704d89/erdos-726/Solution.lean#L36.
The classical estimate of Mertens states that \(\sum_{p\leq n}\frac{1}{p}\sim \log\log n\).
theorem erdos_726.variants.mertens_estimate :
(fun n : ℕ ↦ ∑ p ∈ (range (n + 1)).filter (fun p ↦ p.Prime), (1 : ℝ) / ((p : ℕ) : ℝ))
~[atTop] (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/726.lean, line 59.
Sources
TheoremErdős Problem 727#
Reference: erdosproblems.com/727
Quoted from FormalConjectures/ErdosProblems/727.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/727.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos727.erdos_727
Open: stated without proof.
Let \(k ≥ 2\). Does \(((n+k)!)^2∣(2n)!\) hold for infinitely many \(n\)?
theorem erdos_727 : ∀ k ≥ 2,
Set.Infinite {n : ℕ | (Nat.factorial (n + k)) ^ 2 ∣ Nat.factorial (2 * n)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/727.lean, line 36.
Erdos727.erdos_727.variants.k_2
Open: stated without proof.
It is open even for \(k = 2\). Let \(k = 2\). Does \(((n+k)!)^2∣(2n)!\) hold for infinitely many n?
theorem erdos_727.variants.k_2 :
letI k := 2
Set.Infinite {n : ℕ | (Nat.factorial (n + k)) ^ 2 ∣ Nat.factorial (2 * n)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/727.lean, line 45.
Erdos727.erdos_727.variants.k_1
Solved: stated here without proof.
Balakran proved this holds for \(k = 1\).
Let \(k = 1\). Does \(((n+k)!)^2∣(2n)!\) for infinitely many \(n\)?
theorem erdos_727.variants.k_1 :
letI k := 1
Set.Infinite {n : ℕ | (n + k)! ^ 2 ∣ (2 * n)!}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/727.lean, line 56.
Erdos727.erdos_727.variants.k_1_2
Solved: stated here without proof.
Erdős, Graham, Ruzsa, and Straus observe that the method of Balakran can be further used to prove that there are infinitely many \(n\) such that \((n+k)!(n+1)!∣(2n)!\)
theorem erdos_727.variants.k_1_2 (k : ℕ) (hk : 2 ≤ k) :
Set.Infinite {n : ℕ |
(Nat.factorial (n + k)) * (Nat.factorial (n + 1)) ∣ Nat.factorial (2 * n)}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/727.lean, line 66.
Sources
TheoremErdős Problem 728#
Reference: erdosproblems.com/728
Quoted from FormalConjectures/ErdosProblems/728.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/728.
The file states 1 research or textbook statement: 1 solved.
Erdos728.erdos_728
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos728p.lean.
Let \(\varepsilon\) be sufficiently small and \(C, C' > 0\). Are there integers \(a, b, n\) such that
\[a, b > \varepsilon n\quad a!\, b! \mid n!\, (a + b - n)!, \]and
\[C \log n < a + b - n < C' \log n ?\]Note that the website currently displays a simpler (trivial) version of this problem because \(a + b\) isn't assumed to be in the \(n + O(\log n)\) regime.
Barreto and ChatGPT-5.2 have proved that, for any \(0 < C_1 < C_2\), there are infinitely many \(a, b, n\) with \(b = n/2\), \(a = n/2 + O(\log n)\), and \(C_1 \log n < a + b - n < C_2 \log n\) such that \(a! b! \mid n! (a + b - n)!\)
This appears to answer the question in the spirit it was intended.
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_728 :
∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
∃ a b n : ℕ,
0 < n ∧
ε * n < a ∧
ε * n < b ∧
a ! * b ! ∣ n ! * (a + b - n)! ∧
a + b > n + C * log n ∧
a + b < n + C' * log n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/728.lean, line 52.
Sources
TheoremErdős Problem 729#
References: - erdosproblems.com/729 - [EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. (1975), 83-92. - [Er68c] Erdős, P., Aufgabe 557. Elemente Math. (1968), 111-113.
Quoted from FormalConjectures/ErdosProblems/729.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/729.
The file states 1 research or textbook statement: 1 solved.
Erdos729.erdos_729
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos729.lean.
Let \(C>0\) be a constant. Are there infinitely many integers \(a,b,n\) with \(a+b> n+C\log n\) such that the denominator of
\[\frac{n!}{a!b!}\]contains only primes \(\ll_C 1\)?
Erdős [Er68c] proved that if \(a!b!\mid n!\) then \(a+b\leq n+O(\log n)\). This has been proved in the affirmative by Barreto and Leeham, using ChatGPT and Aristotle, with a modification of the argument used for [728].
theorem erdos_729 :
∀ (C : ℝ) (hC : C > 0),
∃ K ≥ 3, Set.Infinite { T : ℕ × ℕ × ℕ |
let (a, b, n) := T
a > 0 ∧ b > 0 ∧ n > 0 ∧
(a : ℝ) + b > n + C * Real.log n ∧
∀ p, p.Prime → p > K →
padicValNat p ((n.factorial / (a.factorial * b.factorial) : ℚ).den) = 0 }
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/729.lean, line 41.
Sources
TheoremErdős Problem 730#
References: - erdosproblems.com/730 - A129515 - PALOMAR-2026-08-22-000001: a Lean 4 proof that there are infinitely many such pairs, checked by Comparator against the statement
S.Infinitebelow and registered with the Palomar registry. The proof follows an argument posted on the erdosproblems.com forum (Liam Price, 24 June 2026), which shows that there are infinitely many consecutive pairs \((n, n+1)\).
Quoted from FormalConjectures/ErdosProblems/730.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/730.
The file states 3 research or textbook statements: 2 solved and 1 textbook result.
Erdos730.erdos_730
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/03729c9cbb0b602f5a828bb850c85e84c5a6d460/ErdosProblems/Erdos730/FullDensityTheorem.lean#L40.
Are there infinitely many pairs of integers \(n < m\) such that \(\binom{2n}{n}\) and \(\binom{2m}{m}\) have the same set of prime divisors?
Yes: there are infinitely many consecutive pairs \((n, n+1)\). The formal proof registered as [PALOMAR-2026-08-22-000001] proves
S.Infinitefor thisS.
theorem erdos_730 : S.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/730.lean, line 52.
Erdos730.erdos_730.variants.explicit_pairs
Textbook result, proved here.
For example, \((87,88)\) and \((607,608)\) are such pairs.
theorem erdos_730.variants.explicit_pairs :
{(87, 88), (607, 608)} ⊆ S
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/730.lean, line 59.
Erdos730.erdos_730.variants.delta_ne_one
Proved here.
There are examples where \((n, m) ∈ S\) with \(m ≠ n + 1\).
(Found by AlphaProof, although it was implicit already in [A129515])
theorem erdos_730.variants.delta_ne_one : ∃ (n m : ℕ), (n, m) ∈ S ∧ m ≠ n + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/730.lean, line 72.
Sources
TheoremErdős Problem 731#
References: - erdosproblems.com/731 - [EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of \(\binom{2n}{n}\). Math. Comp. 29 (1975), 83-92. PDF
Quoted from FormalConjectures/ErdosProblems/731.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/731.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos731.erdos_731
Open: stated without proof.
Find some reasonable function \(f(n)\) such that, for almost all integers \(n\), the least integer \(m\) such that \(m\nmid \binom{2n}{n}\) satisfies
\[m\sim f(n).\]Here "almost all" means natural density \(1\), and \(m \sim f(n)\) means that for every \(\varepsilon>0\) the set of \(n\) with \(|m/f(n)-1|\lt \varepsilon\) has density \(1\).
theorem erdos_731 : ∀ ε > (0 : ℝ),
{n : ℕ | |(leastNonDivisor n : ℝ) / erdos_731.answer n - 1| < ε}.HasDensity 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/731.lean, line 72.
Erdos731.erdos_731.variants.egrs75
Solved: stated here without proof.
A problem of Erdős, Graham, Ruzsa, and Straus [EGRS75], who say it is 'not hard to show that', for almost all \(n\), the minimal such \(m\) satisfies
\[m=\exp((\log n)^{1/2+o(1)}).\][EGRS75, (8), p. 91] states this as: for every \(\varepsilon>0\), for all \(n\) outside a set of density \(0\), \(\exp((\log n)^{1/2-\varepsilon}) < m < \exp((\log n)^{1/2+\varepsilon})\).
theorem erdos_731.variants.egrs75 : ∀ ε > (0 : ℝ),
{n : ℕ | Real.exp (Real.log n ^ ((1 : ℝ) / 2 - ε)) < (leastNonDivisor n : ℝ) ∧
(leastNonDivisor n : ℝ) < Real.exp (Real.log n ^ ((1 : ℝ) / 2 + ε))}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/731.lean, line 85.
Sources
TheoremErdős Problem 732#
References: - erdosproblems.com/732
Quoted from FormalConjectures/ErdosProblems/732.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/732.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos732.erdos_732.parts.i
Open: stated without proof.
Call a sequence \(1< X_1\leq \cdots \leq X_m\leq n\) block-compatible if there is a pairwise balanced block design \(A_1,\ldots,A_m\subseteq \{1,\ldots,n\}\) such that \(\lvert A_i\rvert=X_i\) for \(1\leq i\leq m\). (A pairwise block design means that every pair in \(\{1,\ldots,n\}\) is contained in exactly one of the \(A_i\).) Are there necessary and sufficient conditions for \((X_i)\) to be block-compatible? Is there some constant \(c>0\) such that for all large \(n\) there are
\[\geq \exp(c n^{1/2}\log n)\]many block-compatible sequences for \(\{1,\ldots,n\}\)?
theorem erdos_732.parts.i :
∀ (n : ℕ) (s : List ℕ), s ∈ Hypergraph.blockSizeProfiles n ↔ erdos_732.parts.i.answer n s
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/732.lean, line 45.
Erdos732.erdos_732.parts.ii
Solved: stated here without proof.
Is there some constant \(c>0\) such that for all large \(n\) there are at least \(\exp(c n^{1/2}\log n)\) block-compatible sequences?
Alon has proved there are at least \(2^{(\frac{1}{2}+o(1))n^{1/2}\log n}\) many sequences which are block-compatible for \(n\).
theorem erdos_732.parts.ii :
∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
Real.exp (c * Real.sqrt n * Real.log n) ≤ (Hypergraph.blockSizeProfiles n).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/732.lean, line 57.
Sources
TheoremErdős Problem 733#
References: - erdosproblems.com/733 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. PDF - [SzTr83] Szemerédi, E. and Trotter, Jr., W. T., Extremal problems in discrete geometry. Combinatorica (1983), 381-392.
Quoted from FormalConjectures/ErdosProblems/733.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/733.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 API statement, counted here but not shown.
Erdos733.erdos_733
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos733.lean#L41.
Call a sequence \(1\lt X_1\leq\cdots\leq X_m\leq n\) line-compatible if there is a set of \(n\) points in \(\mathbb{R}^2\) such that there are \(m\) lines \(\ell_1,\ldots,\ell_m\) containing at least two points, and the number of points on \(\ell_i\) is exactly \(X_i\).
Prove that there are at most
\[\exp(O(n^{1/2}))\]many line-compatible sequences.
Asked by Erdős [Er81] and proved by Szemerédi and Trotter [SzTr83]. We take the lines \(\ell_i\) to be distinct but not necessarily all the lines determined by the points, as on erdosproblems.com; [Er81] uses all the determined lines (
allLinesSequences), so this bound implies his. Finiteness of the set is part of the statement, sinceSet.ncardof an infinite set is \(0\).
theorem erdos_733 :
∃ C : ℝ, 0 < C ∧ ∀ n : ℕ,
(compatibleSequences n).Finite ∧
((compatibleSequences n).ncard : ℝ) ≤ Real.exp (C * Real.sqrt n)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/733.lean, line 103.
Erdos733.erdos_733.variants.limit_exists
Open: stated without proof.
Erdős [Er81] writes that it is 'easy' to prove there are at least
\[\exp(cn^{1/2})\]many such sequences for some constant \(c>0\), but expected proving the upper bound to be difficult. Once it is done, he asked for the existence and value of
\[\lim_{n\to \infty}\frac{\log f(n)}{n^{1/2}},\]where \(f(n)\) counts the number of line-compatible sequences. Does this limit exist?
In [Er81], \(f(n)\) counts the sequences of the numbers of points on all the lines determined by \(n\) points, i.e.
(allLinesSequences n).ncard; this set is finite, as a subset ofcompatibleSequences n.
theorem erdos_733.variants.limit_exists :
∃ c : ℝ, Tendsto
(fun n : ℕ ↦ Real.log ((allLinesSequences n).ncard : ℝ) / Real.sqrt n)
atTop (𝓝 c)
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/733.lean, line 122.
Sources
TheoremErdős Problem 734#
References: - erdosproblems.com/734 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [dBEr48] de Bruijn, N. G. and Erdős, P., On a combinatorial problem. Nederl. Akad. Wetensch., Proc. (1948), 1277--1279 = Indagationes Math. 10, 421--423.
Quoted from FormalConjectures/ErdosProblems/734.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/734.
The file states 1 research or textbook statement: 1 open.
Erdos734.erdos_734
Open: stated without proof.
Find, for all large \(n\), a non-trivial pairwise balanced block design \(A_1,\ldots,A_m\subseteq \{1,\ldots,n\}\) such that, for all \(t\), there are \(O(n^{1/2})\) many \(i\) such that \(\lvert A_i\rvert=t\).
theorem erdos_734 :
∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop,
∃ H : Finset (Finset (Fin n)), H.IsPairwiseBalancedDesign ∧
(∀ e ∈ H, e.card < n) ∧ ∀ t : ℕ,
({e ∈ H | e.card = t}.card : ℝ) ≤ C * Real.sqrt n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/734.lean, line 43.
Sources
TheoremErdős Problem 735#
References: - erdosproblems.com/735 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica 1 (1981), 25-42. PDF - [ABKPR08] Ackerman, E., Buchin, K., Knauer, C., Pinchasi, R. and Rote, G., There are not too many magic configurations. Discrete Comput. Geom. 39 (2008), 3-16. DOI
Quoted from FormalConjectures/ErdosProblems/735.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/735.
The file states 1 research or textbook statement: 1 solved. It also has 1 API statement, counted here but not shown.
Erdos735.erdos_735
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos735/Final.lean#L54.
Given any \(n\) points in \(\mathbb{R}^2\) when can one give positive weights to the points such that the sum of the weights of the points along every line containing at least two points is the same?
This is a problem of Murty [Er81], who conjectured that this is only possible in one of four cases: all points on a line, no three points on a line, \(n-1\) points on a line, and a triangle, the angle bisectors, and the incentre (or a projective equivalent). Ackerman, Buchin, Knauer, Pinchasi and Rote [ABKPR08] proved this conjecture. Conversely, every set in these four cases is magic.
theorem erdos_735 : {S : Finset ℝ² | IsMagic S} = erdos_735.answer
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/735.lean, line 93.
Sources
TheoremErdős Problem 737#
References: - erdosproblems.com/737 - [EHS74] Erdős, P. and Hajnal, A. and Shelah, S., On some general properties of chromatic numbers. Topics in topology (Proc. Colloq., Keszthely, 1972) (1974), 243-255. - [Th83] Thomassen, Carsten, Cycles in graphs of uncountable chromatic number. Combinatorica (1983), 133-134.
Quoted from FormalConjectures/ErdosProblems/737.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/737.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos737.erdos_737
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos737.lean#L1266.
Let \(G\) be a graph with chromatic number \(\aleph_1\). Must there exist an edge \(e\) such that, for all large \(n\), \(G\) contains a cycle of length \(n\) containing \(e\)?
The answer is yes, proved by Thomassen [Th83]. Erdős, Hajnal, and Shelah [EHS74] proved that \(G\) must contain all sufficiently large cycles (see Erdős Problem 594).
theorem erdos_737 :
∀ (V : Type) (G : SimpleGraph V), ChromaticNumberAlephOne G →
∃ e ∈ G.edgeSet, ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
CycleThroughEdgeOfLength G e n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/737.lean, line 65.
Erdos737.erdos_737.variants.uncountable
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos737.lean#L1181.
The title and abstract of [Th83] state the result for graphs of uncountable chromatic number, that is, graphs with no proper colouring by
ℕ. This is stronger thanerdos_737.
theorem erdos_737.variants.uncountable :
∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) →
∃ e ∈ G.edgeSet, ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
CycleThroughEdgeOfLength G e n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/737.lean, line 78.
Sources
TheoremErdős Problem 740: Infinitary version of chromatic number and odd cycles#
Reference: erdosproblems.com/740
Quoted from FormalConjectures/ErdosProblems/740.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/740.
The file states 1 research or textbook statement: 1 open.
Erdos740.erdos_740
Open: stated without proof.
Let \(\mathfrak{m}\) be an infinite cardinal and \(G\) be a graph with chromatic number \(\mathfrak{m}\). Let \(r\geq 1\). Must \(G\) contain a subgraph of chromatic number \(\mathfrak{m}\) which does not contain any odd cycle of length \(\leq r\)?
theorem erdos_740 :
∀ (V : Type*) (G : SimpleGraph V),
ℵ₀ ≤ G.chromaticCardinal →
∀ (r : ℕ),
∃ (H : G.Subgraph), H.coe.chromaticCardinal = G.chromaticCardinal ∧
NoShortOddCycle H.coe r
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/740.lean, line 42.
Sources
TheoremErdős Problem 741#
References: - erdosproblems.com/741 - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
Quoted from FormalConjectures/ErdosProblems/741.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/741.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos741.erdos_741.parts.i
Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/9d492049e42167b0d2fd58a9e91da3bf160172b5/FormalConjectures/ErdosProblems/741.lean#L228.
Let \(A\subseteq \mathbb{N}\) be such that \(A+A\) has positive upper density. Can one always decompose \(A=A_1\sqcup A_2\) such that \(A_1+A_1\) and \(A_2+A_2\) both have positive upper density?
This was proved by the DeepMind prover agent.
theorem erdos_741.parts.i : ∀ A : Set ℕ, 0 < upperDensity (A + A) → ∃ A₁ A₂,
A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < upperDensity (A₁ + A₁)
∧ 0 < upperDensity (A₂ + A₂)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/741.lean, line 46.
Erdos741.erdos_741.variants.lower
Open: stated without proof.
Let \(A\subseteq \mathbb{N}\) be such that \(A+A\) has positive lower density. Can one always decompose \(A=A_1\sqcup A_2\) such that \(A_1+A_1\) and \(A_2+A_2\) both have positive lower density?
theorem erdos_741.variants.lower : ∀ A : Set ℕ, 0 < lowerDensity (A + A) → ∃ A₁ A₂,
A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < lowerDensity (A₁ + A₁)
∧ 0 < lowerDensity (A₂ + A₂)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/741.lean, line 57.
Erdos741.erdos_741.variants.exact_density
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1449.
Let \(A\subseteq \mathbb{N}\) be such that \(A+A\) has positive density in the literal sense that its natural density exists and is positive. Can one always decompose \(A=A_1\sqcup A_2\) such that \(A_1+A_1\) and \(A_2+A_2\) both have positive density in this sense?
This was disproved by the DeepMind prover agent.
theorem erdos_741.variants.exact_density :
¬ ∀ A : Set ℕ, HasPosDensity (A + A) → ∃ A₁ A₂,
A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ HasPosDensity (A₁ + A₁)
∧ HasPosDensity (A₂ + A₂)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/741.lean, line 73.
Erdos741.erdos_741.parts.ii
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1629.
Is there a basis \(A\) of order \(2\) such that if \(A=A_1\sqcup A_2\) then \(A_1+A_1\) and \(A_2+A_2\) cannot both have bounded gaps?
This was proved by DeepMind prover agent.
theorem erdos_741.parts.ii : ∃ A : Set ℕ, IsAddBasisOfOrder (A ∪ {0}) 2 ∧ ∀ A₁ A₂,
A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬ (IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/741.lean, line 88.
Sources
TheoremErdős Problem 742#
References: - erdosproblems.com/742 - [Pl75] Plesník, Ján, Critical graphs of given diameter. Acta Fac. Rerum Natur. Univ. Comenian. Math. 30 (1975), 71-93. - [CaHa79] Caccetta, L. and Häggkvist, R., On diameter critical graphs. Discrete Math. 28 (1979), 223-229. - [Fa87] Fan, Genghua, On diameter 2-critical graphs. Discrete Math. 67 (1987), 235-240. - [Fü92] Füredi, Zoltán, The maximum number of edges in a minimal graph of diameter 2. J. Graph Theory 16 (1992), 81-98.
Quoted from FormalConjectures/ErdosProblems/742.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/742.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 1 test statement, counted here but not shown.
Erdos742.erdos_742
Open: stated without proof.
Murty-Simon Conjecture
Let \(G\) be a graph on \(n\) vertices with diameter \(2\) such that deleting any edge increases the diameter. Is it true that \(G\) has at most \(\lfloor n^2 / 4 \rfloor\) edges? Equality is conjectured to hold for the complete balanced bipartite graph \(K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}\).
The conjecture is resolved up to a finite check: Fan [Fa87] verified it for \(n \leq 24\) and \(n = 26\), and Füredi [Fü92] proved it for all sufficiently large \(n\).
theorem erdos_742 :
∀ (V : Type*) [Fintype V] [DecidableEq V]
(G : SimpleGraph V) [DecidableRel G.Adj], IsDiameter2Critical G →
G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/742.lean, line 58.
Erdos742.variants.plesnik_bound
Solved: stated here without proof.
Plesník [Pl75] proved the bound \(|E(G)| < 3n(n-1)/8\) for any diameter-\(2\)-critical graph on \(n\) vertices.
theorem plesnik_bound (G : SimpleGraph V) [DecidableRel G.Adj] (hG : IsDiameter2Critical G) :
(G.edgeFinset.card : ℝ) < 3 * (Fintype.card V : ℝ) * ((Fintype.card V : ℝ) - 1) / 8
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/742.lean, line 103.
Erdos742.variants.fan_bound
Solved: stated here without proof.
Fan [Fa87] verified the Murty-Simon conjecture for all \(n \leq 24\) and for \(n = 26\).
theorem fan_bound (G : SimpleGraph V) [DecidableRel G.Adj]
(hn : Fintype.card V ≤ 24 ∨ Fintype.card V = 26) (hG : IsDiameter2Critical G) :
G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/742.lean, line 111.
Erdos742.variants.furedi_bound
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos742.lean#L4279.
Füredi [Fü92] proved the Murty-Simon conjecture for all sufficiently large \(n\), that is, there exists \(n_0\) such that every diameter-\(2\)-critical graph on \(n \geq n_0\) vertices has at most \(\lfloor n^2 / 4 \rfloor\) edges.
theorem furedi_bound : ∃ n₀ : ℕ, ∀ (V : Type*) [Fintype V] [DecidableEq V]
(G : SimpleGraph V) [DecidableRel G.Adj],
n₀ ≤ Fintype.card V → IsDiameter2Critical G →
G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/742.lean, line 124.
Sources
TheoremErdős Problem 743#
References: - erdosproblems.com/743 - [ABCHPT21] Allen, Peter and Böttcher, Julia and Clemens, Dennis and Hladký, Jan and Piguet, Diana and Taraz, Anusch, The tree packing conjecture for trees of almost linear maximum degree. arXiv:2106.11720 (2021). - [Bo83] Bollobás, Béla, Some remarks on packing trees. Discrete Math. (1983), 203-204. - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Fi83] Fishburn, P. C., Balanced integer arrays: a matrix packing theorem. J. Combin. Theory Ser. A (1983), 98-101. - [Fi83b] Fishburn, P. C., Packing graphs with odd and even trees. J. Graph Theory (1983), 369-383. - [GyLe78] Gyárfás, A. and Lehel, J., Packing trees of different order into \(K_n\). Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Colloq. Math. Soc. János Bolyai 18 (1978), 463-469. - [JKKO19] Joos, Felix and Kim, Jaehoon and Kühn, Daniela and Osthus, Deryk, Optimal packings of bounded degree trees. J. Eur. Math. Soc. (JEMS) (2019), 3573-3647. - [JaMo24] Janzer, Barnabás and Montgomery, Richard, Packing the largest trees in the tree packing conjecture. arXiv:2403.10515 (2024).
Quoted from FormalConjectures/ErdosProblems/743.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/743.
The file states 8 research or textbook statements: 1 open and 7 solved. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos743.erdos_743
Open: stated without proof.
Let \(T_2,\ldots,T_n\) be a collection of trees such that \(T_k\) has \(k\) vertices. Can we always write \(K_n\) as the edge disjoint union of the \(T_k\)?
A conjecture of Gyárfás, known as the tree packing conjecture. We state it as a packing. For every \(n\) and all trees \(T_k\) on the vertex set
Fin k, \(2 \leq k \leq n\), there are injective maps \(f_k : \{0, \ldots, k - 1\} \to \{0, \ldots, n - 1\}\) such that the graphs \(f_k(T_k)\) are pairwise edge-disjoint (seeIsPacking). Every tree with \(k\) vertices is isomorphic to a tree onFin k, so this covers every collection of trees.A tree with \(k\) vertices has \(k - 1\) edges, and \(\sum_{k=2}^{n} (k - 1) = \binom{n}{2}\) is the number of edges of \(K_n\). Hence the copies \(f_k(T_k)\) of a packing cover every edge of \(K_n\). So a packing is the same as a decomposition of \(K_n\) into copies of \(T_2, \ldots, T_n\).
theorem erdos_743 :
∀ n : ℕ, ∀ T : (k : ℕ) → SimpleGraph (Fin k),
(∀ k ∈ Set.Icc 2 n, (T k).IsTree) → IsPacking n (Set.Icc 2 n) T
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 101.
Erdos743.erdos_743.variants.stars_or_paths
Solved: stated here without proof.
Gyárfás and Lehel [GyLe78] proved that this holds if all but at most \(2\) of the trees are stars, or if all the trees are stars or paths. This variant is the second case: each tree is a star or a path.
Here a star on
Fin kisstarGraph cfor a centrec, and a path is a graph isomorphic topathGraph k.
theorem erdos_743.variants.stars_or_paths (n : ℕ) (T : (k : ℕ) → SimpleGraph (Fin k))
(hT : ∀ k ∈ Set.Icc 2 n, (T k).IsTree ∧
((∃ c : Fin k, T k = starGraph c) ∨ Nonempty (T k ≃g pathGraph k))) :
IsPacking n (Set.Icc 2 n) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 115.
Erdos743.erdos_743.variants.all_but_two_stars
Solved: stated here without proof.
Gyárfás and Lehel [GyLe78] proved that this holds if all but at most \(2\) of the trees are stars, or if all the trees are stars or paths. This variant is the first case.
Here a star on
Fin kisstarGraph cfor a centrec. The two trees that may fail to be stars are \(T_a\) and \(T_b\).
theorem erdos_743.variants.all_but_two_stars (n : ℕ) (T : (k : ℕ) → SimpleGraph (Fin k))
(hT : ∀ k ∈ Set.Icc 2 n, (T k).IsTree)
(hstar : ∃ a b : ℕ, ∀ k ∈ Set.Icc 2 n, k ≠ a → k ≠ b → ∃ c : Fin k, T k = starGraph c) :
IsPacking n (Set.Icc 2 n) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 129.
Erdos743.erdos_743.variants.fishburn
Solved: stated here without proof.
Fishburn [Fi83b] proved this for \(n\leq 9\).
theorem erdos_743.variants.fishburn (n : ℕ) (hn : n ≤ 9) (T : (k : ℕ) → SimpleGraph (Fin k))
(hT : ∀ k ∈ Set.Icc 2 n, (T k).IsTree) :
IsPacking n (Set.Icc 2 n) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 139.
Erdos743.erdos_743.variants.bollobas
Solved: stated here without proof.
Bollobás [Bo83] proved that the smallest \(\lfloor n/\sqrt{2}\rfloor\) many trees can always be packed greedily into \(K_n\).
The smallest trees are \(T_1, \ldots, T_m\) with \(m = \lfloor n/\sqrt{2} \rfloor\). The tree \(T_1\) is a single vertex, so we only pack \(T_2, \ldots, T_m\).
theorem erdos_743.variants.bollobas (n : ℕ) (T : (k : ℕ) → SimpleGraph (Fin k))
(hT : ∀ k ∈ Set.Icc 2 ⌊(n : ℝ) / Real.sqrt 2⌋₊, (T k).IsTree) :
IsPacking n (Set.Icc 2 ⌊(n : ℝ) / Real.sqrt 2⌋₊) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 152.
Erdos743.erdos_743.variants.bounded_degree
Solved: stated here without proof.
Joos, Kim, Kühn, and Osthus [JKKO19] proved that this conjecture holds when the trees have bounded maximum degree. That is, for every \(d\) there is \(N\) such that for all \(n \geq N\) the following holds. If \(T_k\) is a tree with \(k\) vertices and maximum degree at most \(d\) for \(2 \leq k \leq n\), then \(K_n\) decomposes into \(T_2, \ldots, T_n\).
They even allow the first \(o(n)\) trees to have arbitrary maximum degree.
theorem erdos_743.variants.bounded_degree (d : ℕ) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ T : (k : ℕ) → SimpleGraph (Fin k),
(∀ k ∈ Set.Icc 2 n, (T k).IsTree ∧ (T k).maxDegree ≤ d) →
IsPacking n (Set.Icc 2 n) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 167.
Erdos743.erdos_743.variants.almost_linear_degree
Solved: stated here without proof.
Allen, Böttcher, Clemens, Hladký, Piguet, and Taraz [ABCHPT21] proved that this conjecture holds when all the trees have maximum degree \(\leq c\frac{n}{\log n}\) for some constant \(c>0\). That is, there is \(c > 0\) such that for all sufficiently large \(n\) the following holds. If \(T_k\) is a tree with \(k\) vertices and maximum degree at most \(cn/\log n\) for \(2 \leq k \leq n\), then \(K_n\) decomposes into \(T_2, \ldots, T_n\).
theorem erdos_743.variants.almost_linear_degree :
∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, ∀ T : (k : ℕ) → SimpleGraph (Fin k),
(∀ k ∈ Set.Icc 2 n,
(T k).IsTree ∧ ((T k).maxDegree : ℝ) ≤ c * (n : ℝ) / Real.log (n : ℝ)) →
IsPacking n (Set.Icc 2 n) T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 182.
Erdos743.erdos_743.variants.largest_trees
Solved: stated here without proof.
Janzer and Montgomery [JaMo24] have proved that there exists some \(c>0\) such that the largest \(cn\) trees can be packed into \(K_n\).
We state this for all sufficiently large \(n\). The trees are \(T_k\) with \(n - cn < k \leq n\), and we also require \(2 \leq k\).
theorem erdos_743.variants.largest_trees :
∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, ∀ T : (k : ℕ) → SimpleGraph (Fin k),
(∀ k : ℕ, 2 ≤ k → k ≤ n → (n : ℝ) - c * n < k → (T k).IsTree) →
IsPacking n {k : ℕ | 2 ≤ k ∧ k ≤ n ∧ (n : ℝ) - c * n < k} T
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/743.lean, line 197.
Sources
TheoremErdős Problem 745: Second-largest component of a random graph#
Reference: erdosproblems.com/745
At the stated parameter \(p=1/n\), the second-largest component has order \(n^{2/3}\) in probability. The logarithmic bound applies to fixed \(p=\lambda/n\) with \(\lambda>1\).
[Al97] Aldous, D., Brownian excursions, critical random graphs and the multiplicative coalescent. Ann. Probab. 25 (1997), 812–854.
[KSS80] Komlós, J., Sulyok, M. and Szemerédi, E., Second largest component in a random graph. Studia Sci. Math. Hungar. 15 (1980), 391–395.
Quoted from FormalConjectures/ErdosProblems/745.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/745.
The file states 3 research or textbook statements: 3 solved.
Erdos745.erdos_745
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos745.lean.
In \(G(n,1/n)\) the second-largest component has order \(n^{2/3}\) in probability. The two positive constants may depend on the probability tolerance.
theorem erdos_745 :
∀ ε : ℝ, 0 < ε → ∃ c C : ℝ, 0 < c ∧ c < C ∧
∃ N : ℕ, ∀ n : ℕ, N ≤ n →
1 - ε ≤ criticalProbability n (fun G ↦
c * (n : ℝ) ^ (2 / 3 : ℝ) ≤ (secondLargestComponentOrder G : ℝ) ∧
(secondLargestComponentOrder G : ℝ) ≤ C * (n : ℝ) ^ (2 / 3 : ℝ))
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/745.lean, line 93.
Erdos745.erdos_745.variants.supercritical
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos745.lean.
For fixed \(\lambda>1\), every constant above \((\lambda-1-\log\lambda)^{-1}\) gives a logarithmic upper bound with high probability.
theorem erdos_745.variants.supercritical (lam : ℝ) (hlam : 1 < lam) (A : ℝ)
(hA : 1 / (lam - 1 - Real.log lam) < A) :
Filter.Tendsto (fun n : ℕ ↦ probability lam n (fun G ↦
(secondLargestComponentOrder G : ℝ) ≤ A * Real.log (n : ℝ)))
Filter.atTop (𝓝 1)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/745.lean, line 106.
Erdos745.erdos_745.variants.noncritical_asymptotic
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos745.lean.
For each fixed \(\lambda>0\) with \(\lambda\ne1\), the second-largest component size, divided by \(\log n\), converges in probability to \((\lambda-1-\log\lambda)^{-1}\).
theorem erdos_745.variants.noncritical_asymptotic
(lam : ℝ) (hlam : 0 < lam) (hne : lam ≠ 1) :
∀ ε : ℝ, 0 < ε → Filter.Tendsto (fun n : ℕ ↦ probability lam n (fun G ↦
|(secondLargestComponentOrder G : ℝ) / Real.log (n : ℝ) -
1 / (lam - 1 - Real.log lam)| < ε)) Filter.atTop (𝓝 1)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/745.lean, line 118.
Sources
TheoremErdős Problem 747#
References: - erdosproblems.com/747 - [JKV08] Johansson, Anders and Kahn, Jeff and Vu, Van, Factors in random graphs. Random Structures Algorithms (2008), 1-28. - [Ka23] Kahn, Jeff, Asymptotics for Shamir's problem. Adv. Math. (2023), Paper No. 109019, 39.
Quoted from FormalConjectures/ErdosProblems/747.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/747.
The file states 1 research or textbook statement: 1 solved.
Erdos747.erdos_747
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos747.lean.
How large should \(\ell(n)\) be such that, almost surely, a random \(3\)-uniform hypergraph on \(3n\) vertices with \(\ell(n)\) edges must contain \(n\) vertex-disjoint edges?
The precise asymptotic was given by Kahn [Ka23], proving that the threshold is \(\sim n\log n\) (also for the general problem over \(r\)-uniform hypergraphs).
theorem erdos_747 :
∀ ε : ℝ, 0 < ε → ε < 1 →
Tendsto (fun n ↦ Hypergraph.matchingProbability (3 * n) 3
⌊(1 + ε) * erdos_747.answer n⌋₊ n) atTop (𝓝 1) ∧
Tendsto (fun n ↦ Hypergraph.matchingProbability (3 * n) 3
⌊(1 - ε) * erdos_747.answer n⌋₊ n) atTop (𝓝 0)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/747.lean, line 49.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.