Erdős Problem 629 to Erdős Problem 655
TheoremErdős Problem 629#
References: - erdosproblems.com/629 - [ERT80] Erdős, Paul and Rubin, Arthur L. and Taylor, Herbert, Choosability in graphs. Proceedings of the West Coast Conference on Combinatorics, Graph Theory and Computing (1979), Congress. Numer. XXVI (1980), 125-157. PDF - [HMT96] Hanson, Denis and MacGillivray, Gary and Toft, Bjarne, Choosability of bipartite graphs. Ars Combin. (1996), 183-192. - [RaSr00] Radhakrishnan, Jaikumar and Srinivasan, Aravind, Improved bounds and algorithms for hypergraph \(2\)-coloring. Random Structures Algorithms (2000), 4-32.
Quoted from FormalConjectures/ErdosProblems/629.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/629.
The file states 7 research or textbook statements: 1 open and 6 solved. It also has 1 API statement, counted here but not shown.
Erdos629.erdos_629
Open: stated without proof.
The list chromatic number \(\chi_L(G)\) is defined to be the minimal \(k\) such that for any assignment of a list of \(k\) colours to each vertex of \(G\) (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices receive distinct colours.
Determine the minimal number of vertices \(n(k)\) of a bipartite graph \(G\) such that \(\chi_L(G)>k\).
theorem erdos_629 : n = erdos_629.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 64.
Erdos629.erdos_629.variants.ert_bounds
Solved: stated here without proof.
A problem of Erdős, Rubin, and Taylor [ERT80], who proved that
\[2^{k-1}\lt n(k) \lt k^22^{k+2}.\]The chain of inequalities in [ERT80, p. 129] needs \(k \geq 2\), since \(m(1) = 1 = 2^0\); for \(k = 1\) the claim holds because \(n(1) = 2\). The case \(k = 0\) is degenerate (\(n(0) = 1\)).
theorem erdos_629.variants.ert_bounds (k : ℕ) (hk : 1 ≤ k) :
2 ^ (k - 1) < n k ∧ n k < k ^ 2 * 2 ^ (k + 2)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 75.
Erdos629.erdos_629.variants.property_b
Solved: stated here without proof.
They also prove that if \(m(k)\) is the size of the smallest family of \(k\)-sets without property B (i.e. the smallest number of \(k\)-sets in a graph with chromatic number \(3\)) then \(m(k)\leq n(k)\leq m(k+1)\).
[ERT80, p. 129] prints the upper bound as \(2m(k)\); we state that form. Here \(m(k)\) is
Hypergraph.minChromaticEdges k 3, as in Erdős Problem 901. We assume \(k \geq 2\): for \(k = 1\) this is⊤, since singleton edges admit no proper colouring, whereas \(m(1) = 1\).
theorem erdos_629.variants.property_b (k : ℕ) (hk : 2 ≤ k) :
(Hypergraph.minChromaticEdges k 3).toNat ≤ n k ∧
n k ≤ 2 * (Hypergraph.minChromaticEdges k 3).toNat
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 89.
Erdos629.erdos_629.variants.radhakrishnan_srinivasan
Solved: stated here without proof.
The lower bounds on \(m(k)\) by Radhakrishnan and Srinivasan [RaSr00] imply that
\[2^k \left(\frac{k}{\log k}\right)^{1/2}\ll n(k).\]
theorem erdos_629.variants.radhakrishnan_srinivasan :
∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
c * 2 ^ k * Real.sqrt (k / Real.log k) ≤ (n k : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 99.
Erdos629.erdos_629.variants.n_two
Solved: stated here without proof.
Erdős, Rubin, and Taylor [ERT80] proved \(n(2)=6\).
theorem erdos_629.variants.n_two : n 2 = 6
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 108.
Erdos629.erdos_629.variants.n_three
Solved: stated here without proof.
Hanson, MacGillivray, and Toft [HMT96] proved \(n(3)=14\).
theorem erdos_629.variants.n_three : n 3 = 14
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 115.
Erdos629.erdos_629.variants.hmt_recursion
Solved: stated here without proof.
Hanson, MacGillivray, and Toft [HMT96] proved
\[n(k) \leq kn(k-2)+2^k.\]
theorem erdos_629.variants.hmt_recursion (k : ℕ) (hk : 2 ≤ k) :
n k ≤ k * n (k - 2) + 2 ^ k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/629.lean, line 123.
Sources
LemmaErdős Problem 633#
Reference: * erdosproblems.com/633 * [So09] Soifer, Alexander, How Does One Cut a Triangle? I * [So09c] Soifer, Alexander, Is there anything beyond the solution? * [BLZ26] Beeson, Michael, Laczkovich, Miklós, and Zhang, Yan, Solution of Erdős problem 633.
Quoted from FormalConjectures/ErdosProblems/633.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/633.
The file states 4 research or textbook statements: 4 solved. It also has 4 API statements, counted here but not shown.
Erdos633.isCuttable_iff_isSquare_of_linearIndependent
Solved: stated here without proof.
A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles. This is proved in [So09c].
lemma isCuttable_iff_isSquare_of_linearIndependent
(hTsides : LinearIndependent ℤ
![dist (T.points 0) (T.points 1),
dist (T.points 1) (T.points 2),
dist (T.points 2) (T.points 0)])
(hTangles : LinearIndependent ℤ
![∠ (T.points 0) (T.points 1) (T.points 2),
∠ (T.points 1) (T.points 2) (T.points 0),
∠ (T.points 2) (T.points 0) (T.points 1)]) :
IsCuttable n T ↔ n ≠ 0 ∧ IsSquare n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/633.lean, line 66.
Erdos633.erdos_633
Solved: stated here without proof.
Which triangles can only be decomposed into a square number of congruent triangles?
Beeson, Laczkovich, and Zhang [BLZ26] classify the triangles that can be tiled only into a square number of congruent triangles, settling this problem. The classification is too involved to encode in the answer slot here, so the answer is left as
sorryand the reference records the result.
lemma erdos_633 : T ∈ erdos_633.answer ↔
∀ n, IsCuttable n T → IsSquare n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/633.lean, line 89.
Erdos633.IsSimiliCuttable.of_ne_zero_two_three_five
Solved: stated here without proof.
Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5. This is proved in [So09].
lemma IsSimiliCuttable.of_ne_zero_two_three_five (hn₀ : n ≠ 0) (hn₂ : n ≠ 2) (hn₃ : n ≠ 3)
(hn₅ : n ≠ 5) : IsSimiliCuttable n T
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/633.lean, line 110.
Erdos633.exists_isSimiliCuttable_iff_ne_zero_two_three_five
Solved: stated here without proof.
There exists a triangle which isn't simili-cuttable into 0, 2, 3, 5 parts. This is proved in [So09].
lemma exists_isSimiliCuttable_iff_ne_zero_two_three_five :
∃ T, ∀ n, IsSimiliCuttable n T ↔ n ≠ 0 ∧ n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 5
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/633.lean, line 116.
Sources
TheoremErdős Problem 636#
References: - erdosproblems.com/636 - [AlKo09] Alon, N. and Kostochka, A. V., Induced subgraphs with distinct sizes. Random Structures Algorithms 34 (2009), 45-53. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81-85. - [KwSu21] Kwan, M. and Sudakov, B., Proof of a conjecture on induced subgraphs of Ramsey graphs. Trans. Amer. Math. Soc. 372 (2019), 5571-5594. arXiv:1712.05656
Quoted from FormalConjectures/ErdosProblems/636.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/636.
The file states 3 research or textbook statements: 3 solved.
Erdos636.erdos_636
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos636.lean#L739.
Suppose \(G\) is a graph on \(n\) vertices which contains no complete graph or independent set on \(\gg \log n\) many vertices. Must \(G\) contain \(\gg n^{5/2}\) induced subgraphs which pairwise differ in either the number of vertices or the number of edges?
A problem of Erdős, Faudree, and Sós (although in [Er93] Erdős credits this question to Alon and Bollobás). This was proved by Kwan and Sudakov [KwSu21].
theorem erdos_636 :
∀ C > (0 : ℝ), ∃ γ > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < C * Real.log n → (G.indepNum : ℝ) < C * Real.log n →
HasManyDistinctInducedSubgraphs G (γ * (n : ℝ) ^ (5 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/636.lean, line 63.
Erdos636.erdos_636.variants.erdos_faudree_sos
Solved: stated here without proof.
Erdős, Faudree, and Sós proved that there exist \(\gg n^{3/2}\) many such subgraphs, as stated on erdosproblems.com. Section 2 of [KwSu21] describes two short proofs of this weaker bound.
theorem erdos_636.variants.erdos_faudree_sos :
∀ C > (0 : ℝ), ∃ γ > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < C * Real.log n → (G.indepNum : ℝ) < C * Real.log n →
HasManyDistinctInducedSubgraphs G (γ * (n : ℝ) ^ (3 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/636.lean, line 74.
Erdos636.erdos_636.variants.best_possible
Solved: stated here without proof.
Erdős, Faudree, and Sós note that the exponent \(5/2\) would be best possible: there are graphs on \(n\) vertices with no complete graph or independent set on \(\gg \log n\) many vertices which contain only \(O(n^{5/2})\) induced subgraphs that pairwise differ in either the number of vertices or the number of edges. For example, the random graph \(G(n, 1/2)\) has this property with high probability. This is the remark following Theorem 1.1 in [KwSu21], where it is proved in sketch form by a concentration inequality and a union bound; see also [AlKo09, Section 4].
theorem erdos_636.variants.best_possible :
∃ C > (0 : ℝ), ∃ K : ℝ, ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < C * Real.log n ∧ (G.indepNum : ℝ) < C * Real.log n ∧
¬ HasManyDistinctInducedSubgraphs G (K * (n : ℝ) ^ (5 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/636.lean, line 89.
Sources
TheoremErdős Problem 639#
References: - erdosproblems.com/639 - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81-85. - [KeSu04] Keevash, Peter and Sudakov, Benny, On the number of edges not covered by monochromatic copies of a fixed graph. J. Combin. Theory Ser. B (2004), 41-53. - [Py86] Pyber, L., Clique covering of graphs. Combinatorica (1986), 393-398.
Quoted from FormalConjectures/ErdosProblems/639.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/639.
The file states 4 research or textbook statements: 4 solved.
Erdos639.erdos_639
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos639.lean.
Is it true that if the edges of \(K_n\) are 2-coloured then there are at most \(n^2/4\) many edges which do not occur in a monochromatic triangle?
Solved by Erdős, Rousseau, and Schelp for large \(n\), but unpublished. Alon has observed that this also follows from a result of Pyber [Py86], which states that (for large enough \(n\)) at most \(\lfloor n^2/4\rfloor+2\) monochromatic cliques cover all edges of a \(2\)-coloured \(K_n\).
This problem was solved completely by Keevash and Sudakov [KeSu04], who proved that the correct threshold is \(\lfloor n^2/4\rfloor\) for all \(n\geq 7\), is \(\binom{n}{2}\) for \(n\leq 5\), and is \(10\) for \(n=6\).
Since the bound fails for small \(n\) (at \(n=6\) the threshold is \(10 > 6^2/4\)), the statement is formalized in the asymptotic reading in which the problem was posed and solved: for all sufficiently large \(n\), every \(2\)-colouring of the edges of \(K_n\) leaves at most \(n^2/4\) edges not occurring in a monochromatic triangle. Edges of \(K_n\) are the non-diagonal unordered pairs
Sym2 (Fin n); an edge \(\{x, y\}\) occurs in a monochromatic triangle if and only if there is a third vertex \(z\) with \(C(\{x, z\}) = C(\{y, z\}) = C(\{x, y\})\).The linked file proves the bound for every finite vertex type with at least \(10\) vertices, which gives the
atTopreading below, and collects the uncovered edges as the edge set of a graph rather than as a set of pairs.
theorem erdos_639 :
∀ᶠ (n : ℕ) in atTop, ∀ C : Sym2 (Fin n) → Fin 2,
{e : Sym2 (Fin n) | ¬e.IsDiag ∧
∀ x y : Fin n, e = s(x, y) →
¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/639.lean, line 63.
Erdos639.erdos_639.variants.exact
Solved: stated here without proof.
The exact maximum number of uncovered edges is \(\binom{n}{2}\) for \(n\leq 5\), \(10\) for \(n=6\), and \(\lfloor n^2/4\rfloor\) for \(n\geq 7\) [KeSu04, Theorem 1.1].
IsGreateststates both the upper bound and its attainment by a colouring.
theorem erdos_639.variants.exact :
∀ n : ℕ, IsGreatest
(Set.range fun C : Sym2 (Fin n) → Fin 2 => (uncoveredEdges C).ncard)
(if n ≤ 5 then n.choose 2 else if n = 6 then 10 else n ^ 2 / 4)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/639.lean, line 81.
Erdos639.erdos_639.variants.ten_le
Solved: stated here; a Lean proof is at https://github.com/AItoBit/formal-conjectures/blob/0ad11a9f7f83c7ada19d42f1a95964465fb1195f/proofs/erdos639/Bridge639.lean.
Every two-colouring of \(K_n\) with \(n\geq 10\) has at most \(\lfloor n^2/4\rfloor\) uncovered edges [KeSu04, Proposition 2.1].
theorem erdos_639.variants.ten_le :
∀ n : ℕ, 10 ≤ n → ∀ C : Sym2 (Fin n) → Fin 2,
(uncoveredEdges C).ncard ≤ n ^ 2 / 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/639.lean, line 92.
Erdos639.erdos_639.variants.six_vertices
Proved here.
There is a two-colouring of \(K_6\) with ten uncovered edges, exceeding \(6^2/4\).
theorem erdos_639.variants.six_vertices :
∃ C : Sym2 (Fin 6) → Fin 2, (uncoveredEdges C).ncard = 10 ∧
6 ^ 2 / 4 < (uncoveredEdges C).ncard
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/639.lean, line 108.
Sources
TheoremErdős Problem 640#
References: - erdosproblems.com/640 - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81–85, p.84.
Quoted from FormalConjectures/ErdosProblems/640.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/640.
The file states 2 research or textbook statements: 1 open and 1 textbook result.
Erdos640.erdos_640
Open: stated without proof.
For every \(k \geq 3\), does there exist \(f(k)\) such that every finite graph of chromatic number at least \(f(k)\) has an odd cycle whose vertices induce a graph of chromatic number at least \(k\)? The cycle may have chords in the ambient graph.
theorem erdos_640 :
∀ k : ℕ, 3 ≤ k → ∃ N : ℕ, ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
(N : ℕ∞) ≤ G.chromaticNumber → HasHighChromaticOddCycle G k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/640.lean, line 46.
Erdos640.erdos_640.variants.three
Textbook result, stated without proof. A Lean proof is at https://github.com/AItoBit/formal-conjectures/blob/0e6191e205ebdc112d8d5c8ec8ff9a3f7f1b0616/proofs/erdos640/Erdos640.lean.
Every finite graph of chromatic number at least \(3\) has an odd cycle whose vertices induce a graph of chromatic number at least \(3\).
theorem erdos_640.variants.three (n : ℕ) (G : SimpleGraph (Fin n))
(hG : (3 : ℕ∞) ≤ G.chromaticNumber) : HasHighChromaticOddCycle G 3
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/640.lean, line 55.
Sources
TheoremErdős Problem 641#
References: - erdosproblems.com/641 - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Le Matematiche (1992), 231–240. - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81–85, p.84. - [JSS24] Janzer, Barnabás, Steiner, Raphael, and Sudakov, Benny, Chromatic number and regular subgraphs. arXiv:2410.02437 (2024).
Quoted from FormalConjectures/ErdosProblems/641.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/641.
The file states 1 research or textbook statement: 1 solved.
Erdos641.erdos_641
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos641.lean.
Is there some function \(f\) such that for all \(k\geq 1\) if a finite graph \(G\) has chromatic number \(\geq f(k)\) then \(G\) has \(k\) edge disjoint cycles on the same set of vertices?
A problem of Erdős and Hajnal. This was resolved in the negative by Janzer, Steiner, and Sudakov [JSS24] - in fact, this fails even at \(k=2\).
theorem erdos_641 : ¬ ∃ f : ℕ → ℕ, ErdosHajnalProperty f
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/641.lean, line 70.
Sources
TheoremErdős Problem 642#
References: - erdosproblems.com/642 - [CES96] Chen, Guantao and Erdős, Paul and Staton, William, Proof of a conjecture of Bollobás on nested cycles. J. Combin. Theory Ser. B (1996), 38--43. - [DMMS24] Draganić, Nemanja and Methuku, Abhishek and Munhá Correia, David and Sudakov, Benny, Cycles with many chords. Random Structures Algorithms (2024), 3--16. - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81-85.
Quoted from FormalConjectures/ErdosProblems/642.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/642.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 2 test statements and 4 API statements, counted here but not shown.
Erdos642.erdos_642
Open: stated without proof.
Let \(f(n)\) be the maximal number of edges in a graph on \(n\) vertices such that all cycles have more vertices than chords. Is it true that \(f(n)\ll n\)?
A problem of Hamburger and Szegedy. A chord is an edge between two vertices of the cycle which are not consecutive in the cycle.
theorem erdos_642 :
(fun n : ℕ => (maxEdges n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/642.lean, line 62.
Erdos642.erdos_642.variants.upper_bound_n_pow_three_halves
Solved: stated here without proof.
Chen, Erdős, and Staton [CES96] proved \(f(n) \ll n^{3/2}\).
theorem erdos_642.variants.upper_bound_n_pow_three_halves :
(fun n : ℕ => (maxEdges n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/642.lean, line 68.
Erdos642.erdos_642.variants.upper_bound_n_log_pow_eight
Solved: stated here without proof.
Draganić, Methuku, Munhá Correia, and Sudakov [DMMS24] have improved this to
\[f(n) \ll n(\log n)^8.\]
theorem erdos_642.variants.upper_bound_n_log_pow_eight :
(fun n : ℕ => (maxEdges n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ) * Real.log n ^ 8)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/642.lean, line 77.
Sources
TheoremErdős Problem 643#
References: - erdosproblems.com/643 - [Fu84] F\"uredi, Z., Hypergraphs in which all disjoint pairs have distinct unions. Combinatorica (1984), 161--168. - [PiVe09] Pikhurko, Oleg and Verstra\"{e}te, Jacques, The maximum size of hypergraphs without generalized 4-cycles. J. Combin. Theory Ser. A (2009), 637--649. - [HMY26] Huang, Hao, Ma, Jie, and Yang, Tianchi, Extremal hypergraphs without generalized 4-cycles. arXiv:2609.37744 (2026), Theorem 1.2.
Quoted from FormalConjectures/ErdosProblems/643.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/643.
The file states 3 research or textbook statements: 2 open and 1 solved. It also has 1 test statement and 2 API statements, counted here but not shown.
Erdos643.erdos_643.parts.i
Open: stated without proof.
Let \(f(n;t)\) be minimal such that if a \(t\)-uniform hypergraph on \(n\) vertices contains at least \(f(n;t)\) edges then there must be four edges \(A,B,C,D\) such that
\[A\cup B= C\cup D\]and
\[A\cap B=C\cap D=\emptyset.\]Estimate \(f(n;t)\) - in particular, is it true that for \(t\geq 3\)
\[f(n;t)=(1+o(1))\binom{n}{t-1}?\]
theorem erdos_643.parts.i :
∀ t : ℕ, 1 ≤ t →
(fun n ↦ (forcingThreshold n t : ℝ)) ~[atTop] erdos_643.parts.i.answer t
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/643.lean, line 56.
Erdos643.erdos_643.parts.ii
Open: stated without proof.
Is it true that \(f(n;t)=(1+o(1))\binom{n}{t-1}\) for \(t\geq 3\)?
For \(t\geq4\), Huang, Ma, and Yang [HMY26] prove the exact extremal formula below. The case \(t=3\) remains open.
theorem erdos_643.parts.ii :
∀ t : ℕ, 3 ≤ t →
(fun n ↦ (forcingThreshold n t : ℝ)) ~[atTop]
(fun n ↦ (n.choose (t - 1) : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/643.lean, line 68.
Erdos643.erdos_643.variants.exact_t_ge_four
Solved: stated here without proof.
Huang, Ma, and Yang [HMY26, Theorem 1.2] determine the maximum size of an avoiding family for each fixed \(t\geq4\) and all sufficiently large \(n\):
\[\binom{n-1}{t-1}+\left\lfloor\frac{n-1}{t}\right\rfloor.\]The forcing threshold is one larger.
theorem erdos_643.variants.exact_t_ge_four :
∀ t : ℕ, 4 ≤ t → ∀ᶠ n : ℕ in atTop,
Hypergraph.extremalNumber n t (fun H ↦ ¬ H.HasRepeatedDisjointUnion) =
(n - 1).choose (t - 1) + (n - 1) / t
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/643.lean, line 79.
Sources
TheoremErdős Problem 644#
References: - erdosproblems.com/644 - [EFKT92] Erdős, P. and Fon-Der-Flaass, D. and Kostochka, A. V. and Tuza, Zs., Small transversals in uniform hypergraphs. Siberian Adv. Math. (1992), 82-88.
Quoted from FormalConjectures/ErdosProblems/644.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/644.
The file states 3 research or textbook statements: 2 open and 1 textbook result. It also has 1 test statement, counted here but not shown.
Erdos644.erdos_644.variants.elementary_upper_bound
Textbook result, proved here.
For \(r \geq 3\), the transversal bound satisfies \(f(k,r) \leq 2k\).
theorem erdos_644.variants.elementary_upper_bound (k r : ℕ) (hr : 3 ≤ r) :
Hypergraph.subfamilyTransversalBound k r 2 ≤ ((2 * k : ℕ) : ℕ∞)
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/644.lean, line 37.
Erdos644.erdos_644.parts.i
Open: stated without proof.
Let \(f(k,r)\) be minimal such that if \(A_1,A_2,\ldots\) is a family of sets, all of size \(k\), such that for every collection of \(r\) of the \(A_is\) there is some pair \(\{x,y\}\) which intersects all of the \(A_j\), then there is some set of size \(f(k,r)\) which intersects all of the sets \(A_i\). Is it true that
\[f(k,7)=(1+o(1))\frac{3}{4}k?\]
theorem erdos_644.parts.i :
(fun k ↦ ((Hypergraph.subfamilyTransversalBound k 7 2).toNat : ℝ)) ~[atTop]
(fun k ↦ (3 / 4 : ℝ) * k)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/644.lean, line 95.
Erdos644.erdos_644.parts.ii
Open: stated without proof.
Is it true that for any \(r\geq 3\) there exists some constant \(c_r\) such that
\[f(k,r)=(1+o(1))c_rk?\]
theorem erdos_644.parts.ii :
∀ r : ℕ, 3 ≤ r → ∃ c : ℝ, 0 < c ∧
(fun k ↦ ((Hypergraph.subfamilyTransversalBound k r 2).toNat : ℝ)) ~[atTop]
(fun k ↦ c * k)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/644.lean, line 105.
Sources
TheoremErdős Problem 645#
References: - erdosproblems.com/645 - [BrLa99] Brown, Tom C. and Landman, Bruce M., Monochromatic arithmetic progressions with large differences. Bull. Austral. Math. Soc. (1999), 21--35.
Quoted from FormalConjectures/ErdosProblems/645.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/645.
The file states 1 research or textbook statement: 1 solved.
Erdos645.erdos_645
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos645.lean.
If ℕ is \(2\)-coloured then there must exist a monochromatic three-term arithmetic progression \(x,x+d,x+2d\) such that \(d>x\).
This was first proved by Brown and Landman [BrLa99], who in fact show that this is always possible with \(d>f(x)\) for any increasing function \(f\).
This was formalized in Lean by Alexeev using Aristotle and ChatGPT.
theorem erdos_645 (c : ℕ → Bool) : ∃ x d, 0 < x ∧ x < d ∧
(∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/645.lean, line 45.
Sources
TheoremErdős Problem 646#
References: - erdosproblems.com/646 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Be97] Berend, Daniel, On the parity of exponents in the factorization of \(n!\). J. Number Theory (1997), 13-19.
Quoted from FormalConjectures/ErdosProblems/646.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/646.
The file states 1 research or textbook statement: 1 solved.
Erdos646.erdos_646
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos646.lean.
Let \(p_1,\ldots,p_k\) be distinct primes. Are there infinitely many \(n\) such that \(n!\) is divisible by an even power of each of the \(p_i\)?
The answer is yes, proved by Berend [Be97], who further proved that the sequence of such \(n\) has bounded gaps (where the bound depends on the initial set of primes).
theorem erdos_646 :
∀ S : Finset ℕ, (∀ p ∈ S, p.Prime) →
{n : ℕ | ∀ p ∈ S, Even (padicValNat p (n !))}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/646.lean, line 47.
Sources
TheoremErdős Problem 647#
Reference: erdosproblems.com/647
Quoted from FormalConjectures/ErdosProblems/647.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/647.
The file states 4 research or textbook statements: 3 open and 1 solved.
Erdos647.erdos_647
Open: stated without proof.
Let \(\tau(n)\) count the number of divisors of \(n\). Is there some \(n > 24\) such that
\[ \max_{m < n}(m + \tau(m)) \leq n + 2? \]
theorem erdos_647 : ∃ n > 24, ⨆ m : Fin n, m + σ 0 m ≤ n + 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/647.lean, line 37.
Erdos647.erdos_647.variants.twenty_four
Proved here.
This is true for \(n = 24\).
theorem erdos_647.variants.twenty_four : ⨆ m : Fin 24, (m : ℕ) + σ 0 m ≤ 26
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/647.lean, line 42.
Erdos647.erdos_647.variants.lim
Open: stated without proof.
Erdős says 'it is extremely doubtful' that there are infinitely many such \(n\), and in fact suggests that
\[ lim_{n\to\infty} \max_{m < n}(\tau(m) + m − n) = \infty. \]
theorem erdos_647.variants.lim :
atTop.Tendsto (fun n ↦ ⨆ m : Fin n, σ 0 m + m - n) atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/647.lean, line 51.
Erdos647.erdos_647.variants.infinite
Open: stated without proof.
Erdős says it 'seems certain' that for every \(k\) there are infinitely many \(n\) for which
\[ \max_{n−k < m < n}(m + \tau(m)) ≤ n + 2. \]
theorem erdos_647.variants.infinite :
∀ k, { n | ⨆ m : Set.Ioo (n - k) n, ↑m + σ 0 m ≤ n + 2 }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/647.lean, line 61.
Sources
TheoremErdős Problem 648#
References: - erdosproblems.com/648 - [Er95c] Erdős, Paul, Some problems in number theory. Octogon Math. Mag. (1995), 3-5. - [Ca25b] S. Cambie, On Erdős problem #648. arXiv:2503.22691 (2025).
Quoted from FormalConjectures/ErdosProblems/648.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/648.
The file states 1 research or textbook statement: 1 solved.
Erdos648.erdos_648
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos648.lean.
Let \(g(n)\) denote the largest \(t\) such that there exist integers \(2\leq a_1\lt a_2\lt \cdots \lt a_t \lt n\) such that
\[P(a_1)>P(a_2)>\cdots >P(a_t)\]where \(P(m)\) is the greatest prime factor of \(m\). Estimate \(g(n)\).
Stijn Cambie has proved [Ca25b]
\[g(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}.\]Cambie further asks whether there exists a constant \(c\) such that
\[g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}.\]Cambie's proof shows that such a \(c\) must satisfy \(2\leq c\leq 2\sqrt{2}\).
The sequence \(a_1\lt a_2\lt \cdots\lt a_t\) is packaged as a strictly monotone map
a : Fin t → ℕwith \(2\leq a_i\lt n\), the greatest prime factor \(P\) isNat.maxPrimeFac, and \(g(n)\) is the supremum inℕof the achievable lengths \(t\).
theorem erdos_648 :
(fun n => (g n : ℝ)) =Θ[atTop] fun n => Real.sqrt ((n : ℝ) / Real.log (n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/648.lean, line 68.
Sources
TheoremErdős Problem 649#
References: - erdosproblems.com/649 - [Ma35] Mahler, Kurt, Über den grössten Primteiler spezieller Polynome zweiten Grades. Archiv für math. og naturvid (1935). - [Ro64b] Rotkiewicz, André, Sur les nombres naturels \(n\) et \(k\) tels que les nombres \(n\) et \(nk\) sont à la fois pseudopremiers. Atti Accad. Naz. Lincei Rend. Cl. Sci. Fis. Mat. Nat. (8) (1964), 816-818.
Quoted from FormalConjectures/ErdosProblems/649.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/649.
The file states 7 research or textbook statements: 1 open, 3 solved and 3 textbook results.
Erdos649.erdos_649
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos649.lean#L488.
Let \(P(m)\) denote the greatest prime factor of \(m\). Is it true that, for any two primes \(p,q\), there exists some integer \(n\) such that \(P(n)=p\) and \(P(n+1)=q\)?
In fact, the answer to this question as written is easily seen to be no, since there are no solutions to \(2^k\equiv -1\pmod{7}\), and hence this fails with \(p=2\) and \(q=7\). It is possible that Erdős meant to exclude such obstructions, by amending this to 'odd primes' or 'all sufficiently large primes' or such.
The statement below assumes \(p \neq q\): for \(p = q\) no such \(n\) exists, because \(p\) would divide both \(n\) and \(n+1\).
theorem erdos_649 :
¬ ∀ p q : ℕ, p.Prime → q.Prime → p ≠ q →
∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 50.
Erdos649.erdos_649.variants.finite
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos649.lean#L97.
The number of solutions is finite for any fixed \(p,q\) since the largest prime factor of \(n(n+1)\) tends to \(\infty\) (Mahler [Ma35] showed that this is \(\gg \log\log n\), see 368).
theorem erdos_649.variants.finite (p q : ℕ) :
{n : ℕ | n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 62.
Erdos649.erdos_649.variants.no_solution_two_seven
Textbook result, proved here.
In fact, the answer to this question as written is easily seen to be no, since there are no solutions to \(2^k\equiv -1\pmod{7}\), and hence this fails with \(p=2\) and \(q=7\).
theorem erdos_649.variants.no_solution_two_seven :
¬ ∃ n : ℕ, n.maxPrimeFac = 2 ∧ (n + 1).maxPrimeFac = 7
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 71.
Erdos649.erdos_649.variants.tong
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos649.lean#L374.
Even with such amendments, this problem is false in a strong sense: Alan Tong has provided the following elegant elementary proof that, for any given prime \(p\), there are infinitely many primes \(q\) such that this statement is false: let \(m\) be the product of all primes \(\leq p\), and choose a prime \(q\) congruent to \(-1\) modulo \(4m\). If \(p\) is the greatest prime divisor of \(n\) then, using quadratic reciprocity, every prime divisor of \(n\) is a quadratic residue modulo \(q\), and hence \(n\) is a quadratic residue modulo \(q\). On the other hand, since \(q\equiv 3\pmod{4}\) we know that \(-1\) is not a quadratic residue modulo \(q\), and hence \(n\not\equiv -1\pmod{q}\), so it is impossible for \(q\mid n+1\).
theorem erdos_649.variants.tong (p : ℕ) (hp : p.Prime) :
{q : ℕ |
q.Prime ∧ ¬ ∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 104.
Erdos649.erdos_649.variants.tong_question
Open: stated without proof.
Tong asks whether, for any given odd prime \(q\), there are infinitely many primes \(p\) such that there is no integer \(n\) with \(P(n)=p\) and \(P(n+1)=q\).
theorem erdos_649.variants.tong_question :
∀ q : ℕ, q.Prime → Odd q →
{p : ℕ |
p.Prime ∧ ¬ ∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 114.
Erdos649.erdos_649.variants.sampaio
Textbook result, proved here.
Sampaio independently observed that the answer to Erdős' original problem is no if one of the primes can be \(2\) - for example this is false with \(p=19\) and \(q=2\), since if \(n+1=2^k\) and \(19\mid n\) then (since \(2\) is a primitive root modulo \(19\)) we must have \(18\mid k\), and hence \(73\mid 2^{18}-1\mid n\).
theorem erdos_649.variants.sampaio :
¬ ∃ n : ℕ, n.maxPrimeFac = 19 ∧ (n + 1).maxPrimeFac = 2
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 127.
Erdos649.erdos_649.variants.rmm_2020
Textbook result, stated without proof. A Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos649.lean#L1090.
Problem 6 in the 12th Romanian Master of Mathematics Competitions in 2020 was to prove that there exist infinitely many odd primes \(p\) such that, for every \(n\), \(P(n)P(n+1)\neq 2p\).
theorem erdos_649.variants.rmm_2020 :
{p : ℕ | p.Prime ∧ Odd p ∧
∀ n : ℕ, n.maxPrimeFac * (n + 1).maxPrimeFac ≠ 2 * p}.Infinite
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/649.lean, line 159.
Sources
TheoremErdős Problem 650#
References: - erdosproblems.com/650 - [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. - [Er86c] Erdős, P., Some problems on number theory. (1986), 53-67. - [Er95c] Erdős, Paul, Some problems in number theory. Octogon Math. Mag. (1995), 3-5. - [ErSu59] Erdős, Pál and Surányi, János, Bemerkungen zu einer Aufgabe eines mathematischen Wettbewerbs. Mat. Lapok (1959), 39-48. - [VLT26] W. Van Doorn, Y. Li, and Q. Tang, Optimal bounds for an Erdős problem on matching integers to distinct multiples. arXiv:2603.28636 (2026).
Quoted from FormalConjectures/ErdosProblems/650.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/650.
The file states 4 research or textbook statements: 4 solved.
Erdos650.erdos_650.parts.i
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem650.lean.
Let \(f(m)\) be such that if \(A\subseteq \{1,\ldots,N\}\) has \(\lvert A\rvert=m\) then every interval in \([1,\infty)\) of length \(2N\) contains \(\geq f(m)\) many distinct integers \(b_1,\ldots,b_r\) where each \(b_i\) is divisible by some \(a_i\in A\), where \(a_1,\ldots,a_r\) are distinct.
Estimate \(f(m)\).
GPT 5.4 Pro (prompted by He, Li, and Tang) proved \(f(m)\leq \lceil 2\sqrt{m}\rceil\). A corresponding lower bound was given by GPT 5.4 Pro and Aristotle; it is now known (see the paper of van Doorn, Li, and Tang [VLT26]) that
\[f(m) = \min(m, \lceil 2\sqrt{m}\rceil)\]for all \(m\).
This was formalized in Lean by van Doorn using Aristotle.
theorem erdos_650.parts.i (m : ℕ) : f m = min m ⌈2 * Real.sqrt m⌉₊
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/650.lean, line 67.
Erdos650.erdos_650.parts.ii
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem650.lean.
Let \(f(m)\) be such that if \(A\subseteq \{1,\ldots,N\}\) has \(\lvert A\rvert=m\) then every interval in \([1,\infty)\) of length \(2N\) contains \(\geq f(m)\) many distinct integers \(b_1,\ldots,b_r\) where each \(b_i\) is divisible by some \(a_i\in A\), where \(a_1,\ldots,a_r\) are distinct.
In particular is it true that \(f(m)\leq \sqrt{m}\)?
GPT 5.4 Pro (prompted by He, Li, and Tang) proved \(f(m)\leq \lceil 2\sqrt{m}\rceil\). A corresponding lower bound was given by GPT 5.4 Pro and Aristotle; it is now known (see the paper of van Doorn, Li, and Tang [VLT26]) that
\[f(m) = \min(m, \lceil 2\sqrt{m}\rceil)\]for all \(m\).
This was formalized in Lean by van Doorn using Aristotle.
theorem erdos_650.parts.ii : ¬ ∀ m : ℕ, (f m : ℝ) ≤ Real.sqrt m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/650.lean, line 88.
Erdos650.erdos_650.variants.erdos_suranyi
Solved: stated here without proof.
Erdős and Surányi [ErSu59] proved that \(f(m)\geq\sqrt{m}\).
theorem erdos_650.variants.erdos_suranyi (m : ℕ) : Real.sqrt m ≤ (f m : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/650.lean, line 95.
Erdos650.erdos_650.variants.erdos_selfridge
Solved: stated here without proof.
Erdős and Selfridge proved (see [Er78] and [Er86c]) that \(f(m^2)\leq 2m\), which implies \(f(m)\leq 2\lceil \sqrt{m}\rceil\) for all \(m\).
theorem erdos_650.variants.erdos_selfridge (m : ℕ) : f (m ^ 2) ≤ 2 * m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/650.lean, line 103.
Sources
TheoremErdős Problem 651#
References: - erdosproblems.com/651 - [Er97e] Erdős, P., Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [ErSz60] Erdős, P. and Szekeres, G., On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 3-4 (1960/61), 53-62. - [PoZa22] Pohoata, C. and Zakharov, D., Convex polytopes from fewer points. arXiv:2208.04878 (2022). - [Va96] Valtr, P., Several results related to the Erdős-Szekeres theorem. Doctoral dissertation, Charles University, Prague (1996).
Quoted from FormalConjectures/ErdosProblems/651.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/651.
The file states 6 research or textbook statements: 6 solved. It also has 2 API statements, counted here but not shown.
Erdos651.nonempty_cardSet
Solved: stated here without proof.
For \(k \geq 2\) and every \(n\) there is an integer \(N\) such that any \(N\) points in general position in \(\mathbb{R}^k\) contain \(n\) points in convex position. So \(f_k(n)\) is well defined.
This is the higher-dimensional Erdős-Szekeres theorem. For \(n \leq k + 1\) one can take \(N = n\). For larger \(n\) it follows from Ramsey's theorem, which gives \(f_k(n) \leq R_{k+2}(k+3, n)\), see [PoZa22, Section 1].
theorem nonempty_cardSet {k : ℕ} (hk : 2 ≤ k) (n : ℕ) : (cardSet k n).Nonempty
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 103.
Erdos651.erdos_651
Solved: stated here without proof.
Let \(f_k(n)\) denote the smallest integer such that any \(f_k(n)\) points in general position in \(\mathbb{R}^k\) contain \(n\) which determine a convex polyhedron. Is it true that
\[ f_k(n) > (1+c_k)^n \]for some constant \(c_k>0\)?
A problem of Erdős [Er97e]. We read "determine a convex polyhedron" as "are in convex position", and the inequality as holding, with some \(c_k > 0\), for all sufficiently large \(n\). We ask the question for every dimension \(k \geq 3\). The planar case \(k = 2\) is the Erdős-Klein-Szekeres problem (see
erdos_651.variants.planar).The answer is no. Pohoata and Zakharov [PoZa22, Theorem 1.1] proved that \(f_3(n) \leq 2^{o(n)}\), and this implies \(f_k(n) \leq 2^{o(n)}\) for every \(k \geq 3\), see
erdos_651.variants.pohoata_zakharov.
theorem erdos_651 :
¬ ∀ k : ℕ, 3 ≤ k → ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (1 + c) ^ n < (f k n : ℝ)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 124.
Erdos651.erdos_651.variants.pohoata_zakharov
Solved: stated here without proof.
Pohoata and Zakharov [PoZa22, Theorem 1.1] proved that \(ES_3(n) = 2^{o(n)}\), where \(ES_k(n)\) is the function \(f_k(n)\) above: for every \(\varepsilon > 0\) and all large \(n\), any set of at least \(2^{\varepsilon n}\) points in general position in \(\mathbb{R}^3\) contains \(n\) points in convex position. By the projection argument of Valtr [Va96] (see
erdos_651.variants.antitone) the same holds in every dimension \(k \geq 3\) [PoZa22, abstract and Section 1].The theorem gives \(f_k(n) \leq \lceil 2^{\varepsilon n} \rceil\). The form below follows by applying it with \(\varepsilon / 2\).
theorem erdos_651.variants.pohoata_zakharov {k : ℕ} (hk : 3 ≤ k) :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (f k n : ℝ) ≤ (2 : ℝ) ^ (ε * (n : ℝ))
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 139.
Erdos651.erdos_651.variants.subexponential
Solved: stated here without proof.
For every dimension \(k \geq 3\) and every \(c > 0\) one has \(f_k(n) \leq (1+c)^n\) for all large \(n\). This is
erdos_651.variants.pohoata_zakharovwith \(\varepsilon = \log_2(1 + c)\). In particular, for every \(c > 0\) the lower bound \(f_k(n) > (1+c)^n\) fails not only for infinitely many \(n\) but for all large \(n\).
theorem erdos_651.variants.subexponential {k : ℕ} (hk : 3 ≤ k) :
∀ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (f k n : ℝ) ≤ (1 + c) ^ n
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 150.
Erdos651.erdos_651.variants.planar
Solved: stated here without proof.
For \(k = 2\) the lower bound of the question holds: \(f_2(n) > (1+c)^n\) for some \(c > 0\) and all large \(n\). Erdős and Szekeres [ErSz60] proved that \(2^{n-2} + 1 \leq f_2(n)\), see [PoZa22, abstract and Section 1], and \((3/2)^n < 2^{n-2} + 1\) for all \(n \geq 5\). The Erdős-Klein-Szekeres conjecture (Erdős Problem 107) states that \(f_2(n) = 2^{n-2} + 1\) for \(n \geq 3\).
theorem erdos_651.variants.planar :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (1 + c) ^ n < (f 2 n : ℝ)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 162.
Erdos651.erdos_651.variants.antitone
Solved: stated here without proof.
The function \(f_k(n)\) does not increase with the dimension: \(f_{k+1}(n) \leq f_k(n)\) for \(k \geq 2\). Given a set in general position in \(\mathbb{R}^{k+1}\) with at least \(f_k(n)\) points, project it to a generic hyperplane, find \(n\) points in convex position in the projection, and lift them back. This projection argument is due to Valtr [Va96]; see [PoZa22, Section 1, (1)].
The site states that \(f_2(n) > f_3(n) > \cdots\). [PoZa22] gives only the non-strict inequality, so we state that. The strict inequalities fail for small \(n\): for example \(f_2(3) = f_3(3) = 3\).
theorem erdos_651.variants.antitone {k : ℕ} (hk : 2 ≤ k) (n : ℕ) : f (k + 1) n ≤ f k n
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/651.lean, line 176.
Sources
TheoremErdős Problem 652#
References: - erdosproblems.com/652 - [Ma21] Mathialagan, Surya, On bipartite distinct distances in the plane. Electron. J. Combin. 28 (2021), no. 4, Paper No. 4.33, 25 pp. doi:10.37236/9687 - Discussion
Quoted from FormalConjectures/ErdosProblems/652.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/652.
The file states 7 research or textbook statements: 7 solved. It also has 1 test statement, counted here but not shown.
Erdos652.erdos_652
Solved: stated here without proof.
Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) and let \(R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}\), where the points are ordered such that
\[R(x_1)\leq \cdots \leq R(x_n).\]Let \(\alpha_k\) be minimal such that, for all large enough \(n\), there exists a set of \(n\) points with \(R(x_k)\lt \alpha_kn^{1/2}\). Is it true that \(\alpha_k\to \infty\) as \(k\to \infty\)?
Mathialagan [Ma21] proved that given a set \(P\) of \(k\) points and a set \(Q\) of \(n\) points, with \(2\leq k\leq n^{1/3}\), there exists a point in \(P\) which determines \(\gg (kn)^{1/2}\) distances to points in \(Q\).
theorem erdos_652 : Tendsto alpha atTop atTop
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 69.
Erdos652.erdos_652.variants.first
Solved: stated here without proof.
It is trivial that \(R(x_1)=1\) is possible. We require \(n\geq 2\) because a singleton determines no distances to other points.
theorem erdos_652.variants.first (n : ℕ) (hn : 2 ≤ n) :
∃ points : Finset ℝ², points.card = n ∧
∃ point ∈ points, distinctDistancesFrom points point = 1
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 75.
Erdos652.erdos_652.variants.product
Solved: stated here without proof.
We always have \(R(x_1)R(x_2)\gg n\). Equivalently, the same bound holds for any two distinct points of the set.
theorem erdos_652.variants.product :
∃ c : ℝ, 0 < c ∧ ∀ points : Finset ℝ²,
∀ p ∈ points, ∀ q ∈ points, p ≠ q →
c * points.card ≤
(distinctDistancesFrom points p : ℝ) * distinctDistancesFrom points q
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 83.
Erdos652.erdos_652.variants.elekes
Solved: stated here without proof.
Elekes proved that for every \(k\) and \(n\) sufficiently large there exists some set of \(n\) points with \(R(x_k)\ll_k n^{1/2}\).
theorem erdos_652.variants.elekes :
∀ k : ℕ, ∃ a : ℝ, AdmissibleConstant k a
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 93.
Erdos652.erdos_652.variants.mathialagan
Solved: stated here without proof.
Mathialagan [Ma21, Theorem 14] proved that given a set \(P\) of \(k\) points and a set \(Q\) of \(n\) points, with \(2\leq k\leq n^{1/3}\), there exists a point in \(P\) which determines \(\gg (kn)^{1/2}\) distances to points in \(Q\).
theorem erdos_652.variants.mathialagan :
∃ c : ℝ, 0 < c ∧ ∀ P Q : Finset ℝ²,
2 ≤ P.card → P.card ^ 3 ≤ Q.card →
∃ p ∈ P, c * Real.sqrt ((P.card : ℝ) * Q.card) ≤
(Q.image fun q => dist p q).card
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 102.
Erdos652.erdos_652.variants.kth_lower_bound
Solved: stated here without proof.
Mathialagan's bound immediately implies \(R(x_k)\gg (kn)^{1/2}\) for \(2\leq k\leq n^{1/3}\): fewer than \(k\) points have distance count below the bound.
theorem erdos_652.variants.kth_lower_bound :
∃ c : ℝ, 0 < c ∧ ∀ points : Finset ℝ², ∀ k : ℕ,
2 ≤ k → k ^ 3 ≤ points.card →
(points.filter fun point => (distinctDistancesFrom points point : ℝ) <
c * Real.sqrt ((k : ℝ) * points.card)).card < k
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 113.
Erdos652.erdos_652.variants.order_sqrt
Solved: stated here without proof.
Elekes' construction and Mathialagan's lower bound give \(\alpha_k=\Theta(\sqrt k)\), as noted by Zach Hunter in the discussion.
theorem erdos_652.variants.order_sqrt :
∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ᶠ k : ℕ in atTop,
c * Real.sqrt k ≤ alpha k ∧ alpha k ≤ C * Real.sqrt k
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/652.lean, line 123.
Sources
TheoremErdős Problem 653#
Reference: erdosproblems.com/653
Quoted from FormalConjectures/ErdosProblems/653.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/653.
The file states 1 research or textbook statement: 1 open.
Erdos653.erdos_653
Open: stated without proof.
Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) and let \(R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}\), where the points are ordered such that
\[R(x_1)\leq \cdots \leq R(x_n).\]Let \(g(n)\) be the maximum number of distinct values the \(R(x_i)\) can take. Is it true that \(g(n) \geq (1-o(1))n\)?
theorem erdos_653 : ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ n in atTop, (1 - o n) * n ≤ maximalDistinctDistancesFrom n
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/653.lean, line 38.
Sources
TheoremErdős Problem 654#
References: - erdosproblems.com/654 - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [ErPa90] Erdős, P. and Pach, J., Variations on the theme of repeated distances. Combinatorica (1990), 261--269. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Fe26] T. Feng et al, Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems. arXiv:2601.22401 (2026).
Quoted from FormalConjectures/ErdosProblems/654.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/654.
The file states 7 research or textbook statements: 4 open, 2 solved and 1 textbook result.
Erdos654.erdos_654.parts.i
Solved: stated here without proof.
Let \(f(n)\) be such that, given any \(x_1,\ldots,x_n\in \mathbb{R}^2\) with no four points on a circle, there exists some \(x_i\) with at least \(f(n)\) many distinct distances to the other \(x_j\). Is it true that \(f(n) > (1-o(1))n\)?
Erdős asks this in [Er97e]. The answer is no: Aletheia [Fe26] constructed, for every \(m \geq 10\), a set of \(n = 4m\) points with no four on a circle such that every point has fewer than \(\frac{3}{4}n\) distinct distances to the other points. This gives infinitely many \(n\), which is enough to refute the statement with \(\varepsilon = 1/8\). See
Erdos654.erdos_654.variants.feng.
theorem erdos_654.parts.i :
¬ ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n → NoFourConcyclic A →
∃ x ∈ A, (1 - ε) * (n : ℝ) < (distinctDistancesFrom A x : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 51.
Erdos654.erdos_654.parts.ii
Open: stated without proof.
Let \(f(n)\) be as in
erdos_654.parts.i. Is it true that \(f(n) > (\frac{1}{3}+c)n\) for some constant \(c>0\) and all large \(n\)?
theorem erdos_654.parts.ii :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n → NoFourConcyclic A →
∃ x ∈ A, (1 / 3 + c) * (n : ℝ) < (distinctDistancesFrom A x : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 61.
Erdos654.erdos_654.variants.trivial_bound
Textbook result, proved here.
It is trivial that \(f(n) \geq \frac{n-1}{3}\).
In fact every point \(x\) has at least \(\frac{n-1}{3}\) distinct distances to the other points: a circle centred at \(x\) contains at most three other points, since four would lie on a common circle.
theorem erdos_654.variants.trivial_bound (A : Finset ℝ²) (hA : NoFourConcyclic A) :
∀ x ∈ A, ((#A : ℝ) - 1) / 3 ≤ (distinctDistancesFrom A x : ℝ)
Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 74.
Erdos654.erdos_654.variants.feng
Solved: stated here without proof.
Aletheia [Fe26] showed that for every \(m \geq 10\) there is a set of \(n = 4m\) points in \(\mathbb{R}^2\), no four on a circle, such that every point has fewer than \(\frac{3}{4}n = 3m\) distinct distances to the other points.
The construction places \(2m\) points on each of two perpendicular lines, so it is not in general position. Each point has at most \(3m - 1\) distinct distances to the other points.
theorem erdos_654.variants.feng (m : ℕ) (hm : 10 ≤ m) :
∃ A : Finset ℝ², #A = 4 * m ∧ NoFourConcyclic A ∧
∀ x ∈ A, distinctDistancesFrom A x < 3 * m
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 107.
Erdos654.erdos_654.variants.general_position
Open: stated without proof.
Erdős [Er87b] and Erdős and Pach [ErPa90] ask the question of
erdos_654.parts.iiunder the additional assumption that no three points are on a line. Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) with no three points on a line and no four points on a circle. Is there some \(x_i\) with at least \((\frac{1}{3}+c)n\) distinct distances to the other \(x_j\), for some constant \(c>0\) and all large \(n\)?
theorem erdos_654.variants.general_position :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n → InGeneralPosition A →
∃ x ∈ A, (1 / 3 + c) * (n : ℝ) < (distinctDistancesFrom A x : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 120.
Erdos654.erdos_654.variants.general_position_one_sub_eps
Open: stated without proof.
Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) with no three points on a line and no four points on a circle. Is there some \(x_i\) with at least \((1-o(1))n\) distinct distances to the other \(x_j\)?
This is the general-position analogue of
Erdos654.erdos_654.parts.i. The remark on erdosproblems.com notes that the construction of [Fe26], which has all points on two lines, does not settle the version in general position.
theorem erdos_654.variants.general_position_one_sub_eps :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n → InGeneralPosition A →
∃ x ∈ A, (1 - ε) * (n : ℝ) < (distinctDistancesFrom A x : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 134.
Erdos654.erdos_654.variants.erdos_pach
Open: stated without proof.
Erdős and Pach [ErPa90] suggest that the bound \((1-o(1))n\) holds under the assumption that every circle centred at a point \(x_i\) contains at most \(2\) other points \(x_j\). We state this for points in general position (no three on a line and no four on a circle [Er87b, p. 167]), the setting in which [Er87b] and [ErPa90] ask the weaker question. Without the assumption of no three points on a line the statement is false: the sets of [Fe26] satisfy the circle condition.
theorem erdos_654.variants.erdos_pach :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n → InGeneralPosition A →
AtMostTwoPerCircle A → ∃ x ∈ A, (1 - ε) * (n : ℝ) < (distinctDistancesFrom A x : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/654.lean, line 152.
Sources
TheoremErdős Problem 655#
Reference: erdosproblems.com/655
Quoted from FormalConjectures/ErdosProblems/655.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/655.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos655.erdos_655
Solved: stated here; a Lean proof is at https://github.com/AlperTheKing/formal-conjectures/blob/4aaaf544b6ed0ef22580787a8d8a19e85dc49556/FormalConjectures/ErdosProblems/655.lean.
Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) be such that no circle whose centre is one of the \(x_i\) contains three other points. Are there at least
\[(1+c)\frac{n}{2}\]distinct distances determined between the \(x_i\), for some constant \(c>0\) and all \(n\) sufficiently large?
The answer is no: as Zach Hunter observed, the regular
n-gon (npoints equally spaced on a circle) is valid and determines only⌊n/2⌋ < (1+c)n/2distinct distances, for everyc > 0. (In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position was intended; seeerdos_655.variants.general_position.)The disproof — the regular
n-gon construction together with its supporting lemmas — is formalised at the linked commit.
theorem erdos_655 :
¬ ∃ c > (0 : ℝ), ∀ᶠ n in atTop, ∀ (X : Finset ℝ²), #X = n → IsValid X →
(1 + c) * n / 2 ≤ distinctDistances X
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/655.lean, line 53.
Erdos655.erdos_655.variants.general_position
Open: stated without proof.
Let \(x_1,\ldots,x_n\in \mathbb{R}^2\) be such that no circle whose centre is one of the \(x_i\) contains three other points. Are there at least
\[(1+c)\frac{n}{2}\]distinct distances determined between the \(x_i\), for some constant \(c>0\) and all \(n\) sufficiently large?
In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.
theorem erdos_655.variants.general_position :
∃ c > (0 : ℝ), ∀ᶠ n in atTop, ∀ (X : Finset ℝ²), #X = n → IsValid X →
InGeneralPosition X → (1 + c) * n / 2 ≤ distinctDistances X
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/655.lean, line 67.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.