Erdős Problem 172 to Erdős Problem 197
TheoremErdős Problem 172#
References: - erdosproblems.com/172 - [OpenAI26] OpenAI, Monochromatic finite sums and products in the positive integers. OpenAI Math Release preprint (September 2026). github.com/openai/math
Quoted from FormalConjectures/ErdosProblems/172.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/172.
The file states 1 research or textbook statement: 1 solved.
Erdos172.erdos_172
Solved: stated here; a Lean proof is at https://github.com/cadamcat/hindman-sums-products-lean4/blob/3064cac5f9133a968482886ab1c7a1d69c16207f/audit/Erdos172.lean#L18.
Is it true that in any finite colouring of \(\mathbb{N}\) there exist arbitrarily large finite \(A\) such that all sums and products of distinct elements in \(A\) are the same colour?
theorem erdos_172 :
∀ (n : ℕ) (color : ℕ → Fin n) (m), ∃ (A : Finset ℕ), A.card ≥ m ∧ ∃ c, ∀ (S : Finset A),
S.Nonempty → color (∑ x ∈ S, x) = c ∧ color (∏ x ∈ S, x) = c
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/172.lean, line 41.
Sources
TheoremErdős Problem 173#
References: - erdosproblems.com/173 - [Sh76] Shader, L. E., All right triangles are Ramsey in \(E^2\)!. J. Combin. Theory Ser. A (1976), 385-389.
Quoted from FormalConjectures/ErdosProblems/173.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/173.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos173.erdos_173
Open: stated without proof.
In any \(2\)-colouring of \(\mathbb{R}^2\), for all but at most one triangle \(T\) (up to congruence), there is a monochromatic congruent copy of \(T\).
The colouring is arbitrary. No measurability is assumed.
≅compares vertices with the same label, so the conclusion allows a relabellingσ.
theorem erdos_173 : ∀ (c : ℝ² → Fin 2) (T₁ T₂ : Triangle ℝ ℝ²),
¬ HasMonochromaticCopy c T₁ → ¬ HasMonochromaticCopy c T₂ →
∃ σ : Equiv.Perm (Fin 3), T₁.points ∘ σ ≅ T₂.points
Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/173.lean, line 52.
Erdos173.erdos_173.variants.right_triangle
Solved: stated here without proof.
Shader [Sh76] proved that in any \(2\)-colouring of \(\mathbb{R}^2\), every right-angled triangle has a monochromatic congruent copy.
theorem erdos_173.variants.right_triangle (c : ℝ² → Fin 2) (T : Triangle ℝ ℝ²)
(hT : ∠ (T.points 0) (T.points 1) (T.points 2) = Real.pi / 2) :
HasMonochromaticCopy c T
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/173.lean, line 62.
Erdos173.erdos_173.variants.equilateral_exception
Solved: stated here without proof.
The exceptional triangle can exist: colouring the plane in alternating half-open strips of suitable width gives no monochromatic copy of some equilateral triangle.
theorem erdos_173.variants.equilateral_exception : ∃ (c : ℝ² → Fin 2) (T : Triangle ℝ ℝ²),
dist (T.points 0) (T.points 1) = dist (T.points 1) (T.points 2) ∧
dist (T.points 1) (T.points 2) = dist (T.points 2) (T.points 0) ∧
¬ HasMonochromaticCopy c T
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/173.lean, line 72.
Sources
TheoremErdős Problem 174#
References: - erdosproblems.com/174 - [EGMRSS73] Erdős, P. and Graham, R. L. and Montgomery, P. and Rothschild, B. L. and Spencer, J. and Straus, E. G., Euclidean Ramsey Theorems I. J. Comb. Th. A (1973), 341-363. PDF - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. PDF - [FrRo90] Frankl, P. and Rödl, V., A partition property of simplices in Euclidean space. J. Amer. Math. Soc. (1990), 1-7. - [Kr92] Kříž, Igor, All trapezoids are Ramsey. Discrete Math. (1992), 59-62. - [LRW12] Leader, Imre and Russell, Paul A. and Walters, Mark, Transitive sets in Euclidean Ramsey theory. J. Combin. Theory Ser. A (2012), 382-396. arXiv:1012.1350
Quoted from FormalConjectures/ErdosProblems/174.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/174.
The file states 7 research or textbook statements: 3 open and 4 solved. It also has 1 test statement, counted here but not shown.
Erdos174.erdos_174
Open: stated without proof.
A finite set \(A\subset \mathbb{R}^n\) is called Ramsey if, for any \(k\geq 1\), there exists some \(d=d(A,k)\) such that in any \(k\)-colouring of \(\mathbb{R}^d\) there exists a monochromatic copy of \(A\). Characterise the Ramsey sets in \(\mathbb{R}^n\).
A copy of \(A\) is a set congruent to \(A\), as in [EGMRSS73, p. 344].
theorem erdos_174 (n : ℕ) :
{A : Set (EuclideanSpace ℝ (Fin n)) | IsRamsey A} = erdos_174.answer n
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 80.
Erdos174.erdos_174.variants.spherical
Solved: stated here without proof.
Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus [EGMRSS73] proved that every Ramsey set is 'spherical': it lies on the surface of some sphere.
theorem erdos_174.variants.spherical {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n)))
(hA : IsRamsey A) : EuclideanGeometry.Cospherical A
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 89.
Erdos174.erdos_174.variants.graham
Open: stated without proof.
Graham has conjectured that every spherical set is Ramsey.
theorem erdos_174.variants.graham {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n)))
(hA : A.Finite) (hs : EuclideanGeometry.Cospherical A) : IsRamsey A
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 97.
Erdos174.erdos_174.variants.leader_russell_walters
Open: stated without proof.
Leader, Russell, and Walters [LRW12] have alternatively conjectured that a set is Ramsey if and only if it is 'subtransitive': it can be embedded in some higher-dimensional set on which rotations act transitively.
We use the definition of [LRW12]: a subset of a finite set whose symmetry group acts transitively.
theorem erdos_174.variants.leader_russell_walters {n : ℕ}
(A : Set (EuclideanSpace ℝ (Fin n))) (hA : A.Finite) :
IsRamsey A ↔ IsSubtransitive A
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 110.
Erdos174.erdos_174.variants.brick
Solved: stated here without proof.
Sets known to be Ramsey include vertices of \(k\)-dimensional rectangles [EGMRSS73].
This is the case of the vertices
{x | ∀ i, x i = 0 ∨ x i = a i}of a rectangular parallelepiped [EGMRSS73, Cor. 21]; some \(a_i\) may be \(0\) [EGMRSS73, Cor. 22].
theorem erdos_174.variants.brick {n : ℕ} (a : Fin n → ℝ) :
IsRamsey {x : EuclideanSpace ℝ (Fin n) | ∀ i, x i = 0 ∨ x i = a i}
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 122.
Erdos174.erdos_174.variants.simplex
Solved: stated here without proof.
Sets known to be Ramsey include non-degenerate simplices [FrRo90].
A non-degenerate simplex is a set of affinely independent points.
theorem erdos_174.variants.simplex {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n)))
(hA : AffineIndependent ℝ (Subtype.val : A → EuclideanSpace ℝ (Fin n))) :
IsRamsey A
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 132.
Erdos174.erdos_174.variants.trapezoid
Solved: stated here without proof.
Sets known to be Ramsey include trapezoids [Kr92].
We state it for isosceles trapezoids with vertices \((\pm s, 0)\) and \((\pm t, h)\), \(h\neq 0\). A trapezoid that is not isosceles is not spherical, so it is not Ramsey by [EGMRSS73].
theorem erdos_174.variants.trapezoid (s t h : ℝ) (hh : h ≠ 0) :
IsRamsey ({!₂[-s, 0], !₂[s, 0], !₂[-t, h], !₂[t, h]} :
Set (EuclideanSpace ℝ (Fin 2)))
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/174.lean, line 144.
Sources
TheoremErdős Problem 175#
References: - erdosproblems.com/175 - [Sa85] A. Sárközy, On divisors of binomial coefficients, I, J. Number Theory 20 (1985), 70–80. - [GrRa96] A. Granville and O. Ramaré, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients, Mathematika 43 (1996), 73–107. - [Ve95] G. Velammal, Is the binomial coefficient \(\binom{2n}{n}\) square free?, Hardy-Ramanujan Journal 18 (1995), 23–45.
Sárközy proved the assertion for all sufficiently large
n; Granville--Ramaré and Velammal independently proved the full rangen ≥ 5.
Quoted from FormalConjectures/ErdosProblems/175.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/175.
The file states 1 research or textbook statement: 1 solved.
Erdos175.erdos_175
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos175.lean#L678.
Show that, for any \(n\geq 5\), the binomial coefficient \(\binom{2n}{n}\) is not squarefree.
theorem erdos_175 (n : ℕ) (hn : 5 ≤ n) :
¬ Squarefree ((2 * n).choose n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/175.lean, line 46.
Sources
TheoremErdős Problem 178#
References: - erdosproblems.com/178 - [ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Be81] Beck, József, Balancing families of integer sequences. Combinatorica (1981), 209-216. - [Be17] Beck, József, A discrepancy problem: balancing infinite dimensional vectors. Number theory—Diophantine problems, uniform distribution and applications (2017), 61-82.
Quoted from FormalConjectures/ErdosProblems/178.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/178.
The file states 1 research or textbook statement: 1 solved.
Erdos178.erdos_178
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos178.lean.
Let \(A_1,A_2,\ldots\) be an infinite collection of infinite sets of integers, say \(A_i=\{a_{i1}\lt a_{i2}\lt \cdots\}\). Does there exist some \(f:\mathbb{N}\to\{-1,1\}\) such that
\[\max_{m, 1\leq i\leq d} \left\lvert \sum_{1\leq j\leq m} f(a_{ij})\right\rvert \ll_d 1\]for all \(d\geq 1\)?
Erdős remarks 'it seems certain that the answer is affirmative'. This was solved by Beck [Be81]. Recently Beck [Be17] proved that one can replace \(\ll_d 1\) with \(\ll d^{4+\epsilon}\) for any \(\epsilon>0\).
theorem erdos_178 :
∀ (a : ℕ → ℕ → ℕ) (ha : ∀ i, StrictMono (a i)),
∃ f : ℕ → ℤ, (∀ n, f n = 1 ∨ f n = -1) ∧
∀ d : ℕ, ∃ C : ℕ, ∀ m i : ℕ, i < d →
|∑ j ∈ range m, f (a i j)| ≤ ↑C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/178.lean, line 47.
Sources
TheoremErdős Problem 180#
References: - erdosproblems.com/180 - [ErSi82] Erdős, P. and Simonovits, M., Compactness results in extremal graph theory. Combinatorica (1982), 275-288. - [OpenAI26] OpenAI, Ten advances in mathematics and theoretical computer science. (2026).
Quoted from FormalConjectures/ErdosProblems/180.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/180.
The file states 2 research or textbook statements: 2 solved.
Erdos180.erdos_180
Solved: stated here without proof.
If \(\mathcal{F}\) is a finite set of finite graphs then \(\mathrm{ex}(n;\mathcal{F})\) is the maximum number of edges a graph on \(n\) vertices can have without containing any subgraphs from \(\mathcal{F}\). Note that it is trivial that \(\mathrm{ex}(n;\mathcal{F})\leq \mathrm{ex}(n;G)\) for every \(G\in\mathcal{F}\). Is it true that, for every \(\mathcal{F}\), there exists \(G\in\mathcal{F}\) such that
\[\mathrm{ex}(n;G)\ll_{\mathcal{F}}\mathrm{ex}(n;\mathcal{F})?\]This is the Erdős–Simonovits compactness conjecture. The answer is no: OpenAI [OpenAI26] give a family of connected bipartite graphs, none of them acyclic, for which no single member controls the family extremal number. See
erdos_180.variants.counterexample.
theorem erdos_180 :
¬ ∀ family : Finset FiniteGraph,
family.Nonempty → IsCyclicFamily family → IsCompactFamily family
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/180.lean, line 75.
Erdos180.erdos_180.variants.counterexample
Solved: stated here; a Lean proof is at https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/CompactnessAndDegeneracy.lean.
The counterexample: a nonempty family of connected bipartite graphs, none acyclic, that is not compact.
theorem erdos_180.variants.counterexample :
∃ family : Finset FiniteGraph,
family.Nonempty ∧
(∀ forbidden ∈ family,
forbidden.graph.Connected ∧ forbidden.graph.IsBipartite ∧
¬ forbidden.graph.IsAcyclic) ∧
¬ IsCompactFamily family
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/180.lean, line 87.
Sources
TheoremErdős Problem 181#
References: - erdosproblems.com/181 - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Ti22] Tikhomirov, K., A remark on the Ramsey number of the hypercube. arXiv:2208.14568 (2022). - [OpenAI26] OpenAI, The hypercube Ramsey number has linear order. OpenAI Math Release preprint (September 2026). github.com/openai/math
Quoted from FormalConjectures/ErdosProblems/181.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/181.
The file states 1 research or textbook statement: 1 solved.
Erdos181.erdos_181
Solved: stated here; a Lean proof is at https://github.com/cadamcat/hypercube-ramsey-lean4/blob/ad206e1bf8240c28b538dfe72f10364cbc1591da/HypercubeRamsey/Main.lean#L14.
Let \(Q_n\) be the \(n\)-dimensional hypercube graph (so that \(Q_n\) has \(2^n\) vertices and \(n2^{n-1}\) edges). Prove that
\[R(Q_n) \ll 2^n.\]
theorem erdos_181 :
∃ C > (0 : ℝ), ∀ n : ℕ,
(diagonalGraphRamsey (hypercube n) : ℝ) ≤ C * 2 ^ n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/181.lean, line 46.
Sources
TheoremErdős Problem 183#
References: - erdosproblems.com/183 - [Er61] Erdős, P., Graph theory and probability. II. Canad. J. Math. (1961), 346-352. - [OpenAI26] OpenAI, Ten advances in mathematics and theoretical computer science. (2026).
Quoted from FormalConjectures/ErdosProblems/183.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/183.
The file states 2 research or textbook statements: 2 solved.
Erdos183.erdos_183
Solved: stated here; a Lean proof is at https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/MulticolorTriangleRamsey.lean.
Let \(R(3;k)\) be the minimal \(n\) such that if the edges of \(K_n\) are coloured with \(k\) colours then there must exist a monochromatic triangle. Determine
\[\lim_{k\to \infty}R(3;k)^{1/k}.\]There is no finite limit: \(R(3;k)^{1/k}\to\infty\). This was established by OpenAI [OpenAI26] along with the explicit superexponential lower bound in
erdos_183.variants.explicit_lower_bound.
theorem erdos_183 :
Tendsto (fun k : ℕ => (multicolourTriangleRamsey k : ℝ) ^ ((1 : ℝ) / (k : ℝ)))
atTop atTop
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/183.lean, line 59.
Erdos183.erdos_183.variants.explicit_lower_bound
Solved: stated here; a Lean proof is at https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/MulticolorTriangleRamsey.lean.
The explicit bound behind
erdos_183: for every \(k\geq 2\),\[R(3;k)\geq \left(\frac{k^{1/3}}{6e^{38}\log k}\right)^k.\]
theorem erdos_183.variants.explicit_lower_bound :
∀ k : ℕ, 2 ≤ k →
(((1 : ℝ) / (6 * Real.exp 38)) * (k : ℝ) ^ ((1 : ℝ) / 3) / Real.log (k : ℝ)) ^ k ≤
(multicolourTriangleRamsey k : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/183.lean, line 71.
Sources
TheoremErdős Problem 184#
References: - erdosproblems.com/184 - [BM22] Bucić, M. and Montgomery, R., Towards the Erdős-Gallai Cycle Decomposition Conjecture. arXiv:2211.07689 (2022). - [CFS14] Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms (2014), 608-626. - [EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106-112. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [OAI26a] OpenAI, A linear cycle-and-edge decomposition of every graph. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf - [Py85] Pyber, L., An Erdős-Gallai conjecture. Combinatorica (1985), 67-79.
Quoted from FormalConjectures/ErdosProblems/184.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/184.
The file states 6 research or textbook statements: 6 solved.
Erdos184.erdos_184
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/CycleDecomposition/Main.lean#L207.
Any graph on \(n\) vertices can be decomposed into \(O(n)\) many edge-disjoint cycles and edges.
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem erdos_184 :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 62.
Erdos184.erdos_184.variants.n_log_n
Solved: stated here without proof.
Erdős and Gallai [EGP66] proved that \(O(n \log n)\) many cycles and edges suffices.
theorem erdos_184.variants.n_log_n :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ) * Real.log (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 77.
Erdos184.erdos_184.variants.lower_bound
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/394ec1c1ff92bdf2fa10f30d62ae9d0455d3ce20/Proofs/T_Erdos184_erdos_184_variants_lower_bound.lean#L285.
The graph \(K_{3,n-3}\) shows that at least \((1+c)n\) many cycles and edges are required, for some constant \(c>0\).
theorem erdos_184.variants.lower_bound :
∃ c > 0, ∀ᶠ n in atTop,
let G : SimpleGraph (Fin n) := fromRel (fun (i j : Fin n) => (i : ℕ) < 3 ∧ 3 ≤ (j : ℕ));
∀ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) →
IsDecomposition G D →
(1 + c) * (n : ℝ) ≤ (D.card : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 94.
Erdos184.erdos_184.variants.covering
Solved: stated here without proof.
In [Er71] Erdős suggests that only \(n-1\) many cycles and edges are required if we do not require them to be edge-disjoint. Pyber [Py85] proved this.
theorem erdos_184.variants.covering :
∀ {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
(⋃ H ∈ D, H.edgeSet) = G.edgeSet ∧
(D.card : ℝ) ≤ (Fintype.card V : ℝ) - 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 109.
Erdos184.erdos_184.variants.bucic_montgomery
Solved: stated here without proof.
Before [OAI26a], the best bound was due to Bucić and Montgomery [BM22], who prove that \(O(n\log^* n)\) many cycles and edges suffice, where \(\log^*\) is the iterated logarithm function.
theorem erdos_184.variants.bucic_montgomery :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ) * (Real.iteratedLog (n : ℝ) : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 123.
Erdos184.erdos_184.variants.conlon_fox_sudakov
Solved: stated here without proof.
Conlon, Fox, and Sudakov [CFS14] proved that \(O_\epsilon(n)\) cycles and edges suffice if \(G\) has minimum degree at least \(\epsilon n\), for any \(\epsilon>0\).
theorem erdos_184.variants.conlon_fox_sudakov :
∀ ε > 0, ∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
(G.minDegree : ℝ) ≥ ε * (Fintype.card V : ℝ) →
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/184.lean, line 139.
Sources
TheoremErdős Problem 185#
References: - erdosproblems.com/185 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique (1991), 64-119.
Quoted from FormalConjectures/ErdosProblems/185.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/185.
The file states 2 research or textbook statements: 2 solved.
Erdos185.erdos_185
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos185.lean#L49.
Let \(f_3(n)\) be the maximal size of a subset of \(\{0,1,2\}^n\) which contains no three points on a line. Is it true that \(f_3(n)=o(3^n)\)?
Originally considered by Moser. It is trivial that \(f_3(n)\geq R_3(3^n)\), the maximal size of a subset of \(\{1,\ldots,3^n\}\) without a three-term arithmetic progression. Moser showed that
\[f_3(n) \gg \frac{3^n}{\sqrt{n}}.\]The answer is yes, which is a corollary of the density Hales-Jewett theorem, proved by Furstenberg and Katznelson [FuKa91].
theorem erdos_185 : (fun n : ℕ => (f3 n : ℝ)) =o[atTop] fun n : ℕ => (3 : ℝ) ^ n
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/185.lean, line 60.
Erdos185.erdos_185.variants.moser
Solved: stated here without proof.
Moser showed that \(f_3(n) \gg \frac{3^n}{\sqrt{n}}\).
theorem erdos_185.variants.moser :
(fun n : ℕ => (3 : ℝ) ^ n / √n) =O[atTop] fun n : ℕ => (f3 n : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/185.lean, line 65.
Sources
TheoremErdős Problem 186#
References: - erdosproblems.com/186 - [Bo89] Bosznay, Á. P., On the lower estimation of nonaveraging sets. Acta Math. Hungar. (1989), 155-157. - [ErSa90] Erdős, P. and Sárközy, A., On a problem of Straus. Disorder in physical systems (1990), 55-66. - [PhZa24] Pham, H. T. and Zakharov, D., Sharp bound for the Erdős–Straus non-averaging set problem. arXiv:2410.14624 (2024).
Quoted from FormalConjectures/ErdosProblems/186.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/186.
The file states 4 research or textbook statements: 4 solved. It also has 2 test statements and 1 API statement, counted here but not shown.
Erdos186.erdos_186
Solved: stated here without proof.
Let \(F(N)\) be the maximal size of \(A\subseteq \{1,\ldots,N\}\) which is 'non-averaging', so that no \(n\in A\) is the arithmetic mean of at least two elements in \(A\). What is the order of growth of \(F(N)\)?
It is known that \(N^{1/4}\ll F(N) \ll N^{1/4+o(1)}\): the lower bound is due to Bosznay [Bo89] and the upper bound to Pham and Zakharov [PhZa24, Theorem 1]. So \(\log F(N)/\log N\to 1/4\).
theorem erdos_186 :
Tendsto (fun N : ℕ ↦ Real.log (F N) / Real.log N) atTop (𝓝 (1 / 4))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/186.lean, line 78.
Erdos186.erdos_186.variants.pham_zakharov
Solved: stated here without proof.
Pham and Zakharov [PhZa24, Theorem 1] proved that every non-averaging subset of \(\{1,\ldots,N\}\) has size at most \(N^{1/4+o(1)}\).
theorem erdos_186.variants.pham_zakharov :
∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, (F N : ℝ) ≤ (N : ℝ) ^ ((1 : ℝ) / 4 + ε)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/186.lean, line 87.
Erdos186.erdos_186.variants.bosznay
Solved: stated here without proof.
The lower bound \(N^{1/4}\ll F(N)\) is due to Bosznay [Bo89].
theorem erdos_186.variants.bosznay :
∃ c : ℝ, 0 < c ∧ ∀ᶠ N : ℕ in atTop, c * (N : ℝ) ^ ((1 : ℝ) / 4) ≤ F N
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/186.lean, line 93.
Erdos186.erdos_186.variants.erdos_sarkozy
Solved: stated here without proof.
The original upper bound of Erdős and Sárközy [ErSa90] was \(F(N)\ll (N\log N)^{1/2}\).
theorem erdos_186.variants.erdos_sarkozy :
∃ C : ℝ, 0 < C ∧ ∀ᶠ N : ℕ in atTop, (F N : ℝ) ≤ C * Real.sqrt ((N : ℝ) * Real.log N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/186.lean, line 99.
Sources
TheoremErdős Problem 188#
References: - erdosproblems.com/188 - [EGMRSS75] Erdős, P. and Graham, R. L. and Montgomery, P. and Rothschild, B. L. and Spencer, J. and Straus, E. G., Euclidean {R}amsey theorems. {II}. (1975), 529--557. - [Ts17] Tsaturian, Sergei, A {E}uclidean {R}amsey result in the plane. Electron. J. Combin. (2017), Paper No. 4.35, 9.
Quoted from FormalConjectures/ErdosProblems/188.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/188.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos188.erdos_188
Open: stated without proof.
What is the smallest \(k\) such that \(\mathbb{R}^2\) can be red/blue coloured with no pair of red points unit distance apart, and no \(k\)-term arithmetic progression of blue points with distance 1?
theorem erdos_188 : IsLeast s erdos_188.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/188.lean, line 50.
Erdos188.erdos_188.variants.nonempty
Solved: stated here without proof.
Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 14, 15):
It has been shown that there is a large \(M\) so that it is possible to partition \(\mathbb{E}^2\) into two sets \(A\) and \(B\) so that \(A\) contains no pair of points with distance 1 and \(B\) contains no A.P. of length \(M\).
theorem erdos_188.variants.nonempty : s.Nonempty
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/188.lean, line 61.
Erdos188.erdos_188.variants.estimate
Solved: stated here without proof.
Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 15):
How small can \(M\) be made? The only estimate currently known is that \(M \le 10000000\) (more or less). In the other direction, it has just been shown by R. Juhász [Ju (79)] that we must have \(M \ge 5\).
theorem erdos_188.variants.estimate : (∀ k, k ∈ s → 5 ≤ k) ∧ (∃ k ∈ s, k ≤ 10000000)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/188.lean, line 71.
Sources
TheoremErdős Problem 189#
Reference: erdosproblems.com/189
Quoted from FormalConjectures/ErdosProblems/189.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/189.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos189.erdos_189
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos189.lean.
If \(\mathbb{R}^2\) is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area?
Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.)
Solved (with answer
False, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero).This was formalized in Lean by Alexeev and Kovac using Aristotle.
theorem erdos_189 :
¬ Erdos189For
(fun a b c d ↦
line[ℝ, a, b].direction ⟂ line[ℝ, b, c].direction ∧
line[ℝ, b, c].direction ⟂ line[ℝ, c, d].direction ∧
line[ℝ, c, d].direction ⟂ line[ℝ, d, a].direction)
(fun a b c d ↦ dist a b * dist b c)
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/189.lean, line 57.
Erdos189.erdos_189.variants.square
Solved: stated here without proof.
Graham claims this is "easy to see".
theorem erdos_189.variants.square :
¬ Erdos189For
(fun a b c d ↦
line[ℝ, a, b].direction ⟂ line[ℝ, b, c].direction ∧
line[ℝ, b, c].direction ⟂ line[ℝ, c, d].direction ∧
line[ℝ, c, d].direction ⟂ line[ℝ, d, a].direction ∧
dist a b = dist b c)
(fun a b c d ↦ dist a b * dist b c)
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/189.lean, line 68.
Erdos189.erdos_189.variants.parallelogram
Open: stated without proof.
Seems to be open, as of January 2025.
theorem erdos_189.variants.parallelogram :
¬ Erdos189For
(fun a b c d ↦
line[ℝ, a, b] ∥ line[ℝ, c, d] ∧
line[ℝ, a, d] ∥ line[ℝ, b, c])
(fun a b c d ↦ dist a b * dist b c * (∡ a b c).sin)
Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/189.lean, line 82.
Sources
TheoremErdős Problem 191#
References: - erdosproblems.com/191 - [ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Ro03] Rödl, Vojtěch, On homogeneous sets of positive integers. J. Combin. Theory Ser. A (2003), 229-240. - [CFS13] Conlon, David and Fox, Jacob and Sudakov, Benny, Two extensions of Ramsey's theorem. Duke Math. J. (2013), 2903-2927.
Quoted from FormalConjectures/ErdosProblems/191.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/191.
The file states 4 research or textbook statements: 4 solved.
Erdos191.erdos_191
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos191.lean#L1272.
Let \(C>0\) be arbitrary. Is it true that, if \(n\) is sufficiently large depending on \(C\), then in any \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) there exists some \(X\subseteq \{2,\ldots,n\}\) such that \(\binom{X}{2}\) is monochromatic and
\[\sum_{x\in X}\frac{1}{\log x}\geq C?\]The answer is yes, which was proved by Rödl [Ro03]. In the same article Rödl also proved a lower bound for this problem, constructing, for all \(n\), a \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) such that if \(X\subseteq \{2,\ldots,n\}\) is such that \(\binom{X}{2}\) is monochromatic then
\[\sum_{x\in X}\frac{1}{\log x}\ll \log\log\log n.\]In the same paper Rödl proves that the answer to the main problem is negative if we consider \(3\)-colourings.
This bound is best possible, as proved by Conlon, Fox, and Sudakov [CFS13], who proved that, if \(n\) is sufficiently large, then in any \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) there exists some \(X\subseteq \{2,\ldots,n\}\) such that \(\binom{X}{2}\) is monochromatic and
\[\sum_{x\in X}\frac{1}{\log x}\geq 2^{-8}\log\log\log n.\]A \(2\)-colouring of the pairs of \(\{2,\ldots,n\}\) is a graph
Gon this vertex set; a monochromatic set is a clique or an independent set ofG.
theorem erdos_191 : ∀ C : ℝ, 0 < C → ∀ᶠ n : ℕ in atTop,
∀ G : SimpleGraph (Finset.Icc 2 n), ∃ X : Finset (Finset.Icc 2 n),
(G.IsClique X ∨ G.IsIndepSet X) ∧ C ≤ ∑ x ∈ X, 1 / Real.log (x : ℕ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/191.lean, line 69.
Erdos191.erdos_191.variants.conlon_fox_sudakov
Solved: stated here without proof.
Conlon, Fox, and Sudakov [CFS13] proved that, if \(n\) is sufficiently large, then in any \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) there exists some \(X\subseteq \{2,\ldots,n\}\) such that \(\binom{X}{2}\) is monochromatic and
\[\sum_{x\in X}\frac{1}{\log x}\geq 2^{-8}\log\log\log n.\]
theorem erdos_191.variants.conlon_fox_sudakov : ∀ᶠ n : ℕ in atTop,
∀ G : SimpleGraph (Finset.Icc 2 n), ∃ X : Finset (Finset.Icc 2 n),
(G.IsClique X ∨ G.IsIndepSet X) ∧
2 ^ (-8 : ℤ) * Real.log (Real.log (Real.log n)) ≤ ∑ x ∈ X, 1 / Real.log (x : ℕ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/191.lean, line 81.
Erdos191.erdos_191.variants.rodl_upper
Solved: stated here without proof.
Rödl [Ro03] constructed, for all \(n\), a \(2\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) such that if \(X\subseteq \{2,\ldots,n\}\) is such that \(\binom{X}{2}\) is monochromatic then
\[\sum_{x\in X}\frac{1}{\log x}\ll \log\log\log n.\]
theorem erdos_191.variants.rodl_upper : ∃ c : ℝ, ∀ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Finset.Icc 2 n), ∀ X : Finset (Finset.Icc 2 n),
G.IsClique X ∨ G.IsIndepSet X →
∑ x ∈ X, 1 / Real.log (x : ℕ) ≤ c * Real.log (Real.log (Real.log n))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/191.lean, line 93.
Erdos191.erdos_191.variants.three_colours
Solved: stated here without proof.
Rödl [Ro03] proved that the answer to erdős_191 is negative if we consider \(3\)-colourings: there is a constant \(C\) such that for every \(n\) some \(3\)-colouring of \(\binom{\{2,\ldots,n\}}{2}\) has \(\sum_{x\in X}\frac{1}{\log x} < C\) for every monochromatic \(X\).
theorem erdos_191.variants.three_colours : ∃ C : ℝ, ∀ n : ℕ,
∃ c : Sym2 (Finset.Icc 2 n) → Fin 3, ∀ X : Finset (Finset.Icc 2 n),
(∃ i : Fin 3, ∀ x ∈ X, ∀ y ∈ X, x ≠ y → c s(x, y) = i) →
∑ x ∈ X, 1 / Real.log (x : ℕ) < C
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/191.lean, line 106.
Sources
TheoremErdős Problem 192#
References: - erdosproblems.com/192 - [ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ke92] Keränen, Veikko, Abelian squares are avoidable on \(4\) letters. Automata, languages and programming (Vienna, 1992) (1992), 41-52. - [FiPu23] Fici, Gabriele and Puzynina, Svetlana, Abelian combinatorics on words: a survey. Comput. Sci. Rev. (2023), Paper No. 100532, 21.
Quoted from FormalConjectures/ErdosProblems/192.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/192.
The file states 1 research or textbook statement: 1 solved.
Erdos192.erdos_192
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos192.lean#L39.
Let \(A=\{a_1,a_2,\ldots\}\subset \mathbb{R}^d\) be an infinite sequence such that \(a_{i+1}-a_i\) is a positive unit vector (i.e. is of the form \((0,0,\ldots,1,0,\ldots,0)\)). For which \(d\) must \(A\) contain a three-term arithmetic progression?
This is true for \(d\leq 3\) and false for \(d\geq 4\).
This problem is equivalent to one on 'abelian squares' (see 231). In particular \(A\) can be interpreted as an infinite string over an alphabet with \(d\) letters (each letter describining which of the \(d\) possible steps is taken at each point). An abelian square in a string \(s\) is a pair of consecutive blocks \(x\) and \(y\) appearing in \(s\) such that \(y\) is a permutation of \(x\). The connection comes from the observation that \(p,q,r\in A\subset \mathbb{R}^d\) form a three-term arithmetic progression if and only if the string corresponding to the steps from \(p\) to \(q\) is a permutation of the string corresponding to the steps from \(q\) to \(r\).
This problem is therefore equivalent to asking for which \(d\) there exists an infinite string over \(\{1,\ldots,d\}\) with no abelian squares. An infinite string without abelian squares was constructed when \(d=4\) by Keränen [Ke92]. We refer to a recent survey by Fici and Puzynina [FiPu23] for more background and related results.
theorem erdos_192 : {d : ℕ | ∀ a : ℕ → Fin d → ℝ, IsPositiveUnitWalk a →
∃ x ∈ Set.range a, ∃ y ∈ Set.range a, ∃ z ∈ Set.range a, x ≠ y ∧ ∀ j, x j + z j = 2 * y j} =
erdos_192.answer
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/192.lean, line 70.
Sources
TheoremErdős Problem 193#
References: - erdosproblems.com/193 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [GeRa79] Gerver, Joseph L. and Ramsey, L. Thomas, "On certain sequences of lattice points." Pacific J. Math. (1979), 357-363. - [CaKa26] Cambie, Stijn and Kalviainen, Erik, "An infinite small-step Z³-walk with no collinear triple." arXiv:2609.01766.
Quoted from FormalConjectures/ErdosProblems/193.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/193.
The file states 2 research or textbook statements: 2 solved.
Erdos193.erdos_193
Solved: stated here; a Lean proof is at https://github.com/ekalvi/erdos-193/blob/fca4e1bd2b423c000a6bef18cf2f3bc0f4bd363e/formal/Hilbert193/Hilbert193/Continuity.lean#L64-L72.
Let \(S \subseteq \mathbb{Z}^3\) be a finite set and let \(A = \lbrace a_1, a_2, \ldots \rbrace\) be an infinite \(S\)-walk, so that \(a_{i+1} - a_i \in S\) for all \(i\). Must \(A\) contain three collinear points?
Cambie and Kalviainen [CaKa26] answered this question in the negative by constructing an infinite walk in \(\mathbb{Z}^3\) with a finite set of steps and no three collinear points.
theorem erdos_193 :
¬ ∀ S : Set (Fin 3 → ℤ), S.Finite →
/- The statement's $A = \lbrace a_1, a_2, \ldots \rbrace$ is an infinite set.
If the sequence only takes finitely many values, one value has to repeat infinitely many
times, which would yield a trivial collinear triple (x, x, x). In this case, the conjecture
would hold for degenerate S-walks. Another case is constant S-walks, which would render the
conjecture trivially false (finite loop ranges have no 3 distinct points).
Assuming the authors intend to stay away from these degenerate cases, we formalize this by
requiring an infinite range (and require distinct points). -/
∀ a : ℕ → Fin 3 → ℤ, IsSWalk S a → (range a).Infinite →
HasCollinearTriple ℚ (range (fun n ↦ (↑) ∘ a n : ℕ → Fin 3 → ℚ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/193.lean, line 58.
Erdos193.erdos_193_z2
Solved: stated here without proof.
[GeRa79] showed that the answer is yes for \(\mathbb{Z}^2\)
theorem erdos_193_z2 :
∀ S : Set (Fin 2 → ℤ), S.Finite →
∀ a : ℕ → Fin 2 → ℤ, IsSWalk S a → (range a).Infinite →
HasCollinearTriple ℚ (range (fun n ↦ (↑) ∘ a n : ℕ → Fin 2 → ℚ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/193.lean, line 77.
Sources
TheoremErdős Problem 194#
References: - erdosproblems.com/194 - [ABJ11] Ardal, H. and Brown, T. and Jungić, V., Chaotic orderings of the rationals and reals. Amer. Math. Monthly (2011), 921-925.
Quoted from FormalConjectures/ErdosProblems/194.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/194.
The file states 1 research or textbook statement: 1 solved.
Erdos194.erdos_194
Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/ster-oc/ffe9e4fa1b813111f40c0e417bbe8be0/raw/6f748a76e55d47e24ca319a9c00fd20ab79422bb/Erdos194.lean.
Let \(k\geq 3\). Must any ordering of \(\mathbb{R}\) contain a monotone \(k\)-term arithmetic progression, that is, some \(x_1 \lt \cdots < x_k\) which forms an increasing or decreasing \(k\)-term arithmetic progression?
The answer is no, even for \(k=3\), as shown by Ardal, Brown, and Jungić [ABJ11].
The answer is no, even for \(k=3\), as shown by Ardal, Brown, and Jungić [ABJ11].
theorem erdos_194 :
¬ ∀ k ≥ 3, ∀ r : ℝ → ℝ → Prop, IsStrictTotalOrder ℝ r →
∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Pairwise r ∨ s.Pairwise (flip r))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/194.lean, line 42.
Sources
TheoremErdős Problem 195#
References: - erdosproblems.com/195 - [Ad22] Adenwalla, S., Avoiding Monotone Arithmetic Progressions in Permutations of Integers. arXiv:2211.04451 (2022). - [Ge19] Geneson, Jesse, Forbidden arithmetic progressions in permutations of subsets of the integers. Discrete Math. (2019), 1489-1491.
Quoted from FormalConjectures/ErdosProblems/195.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/195.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos195.erdos_195
Open: stated without proof.
What is the largest \(k\) such that in any permutation of \(\mathbb{Z}\) there must exist a monotone \(k\)-term arithmetic progression \(x_1 < \cdots < x_k\)?
Here a permutation of \(\mathbb{Z}\) is a one-sided arrangement \(a_1, a_2, a_3, \ldots\) of the integers, i.e. a bijection \(\mathbb{N} \to \mathbb{Z}\), and a monotone \(k\)-term arithmetic progression is a subsequence \(a_{i_1}, \ldots, a_{i_k}\) with \(i_1 < \cdots < i_k\) forming an increasing or decreasing arithmetic progression.
theorem erdos_195 :
erdos_195.answer = sSup {k : ℕ | ∀ f : ℕ ≃ ℤ, HasMonotoneAP f k}
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/195.lean, line 47.
Erdos195.erdos_195.variants.leq_5_bound
Solved: stated here without proof.
Geneson [Ge19] proved that k ≤ 5.
theorem erdos_195.variants.leq_5_bound :
5 ≥ sSup {k : ℕ | ∀ f : ℕ ≃ ℤ, HasMonotoneAP f k}
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/195.lean, line 55.
Erdos195.erdos_195.variants.leq_4_bound
Solved: stated here without proof.
Adenwalla [Ad22] proved that k ≤ 4.
theorem erdos_195.variants.leq_4_bound :
4 ≥ sSup {k : ℕ | ∀ f : ℕ ≃ ℤ, HasMonotoneAP f k}
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/195.lean, line 63.
Sources
TheoremErdős Problem 196#
References: - erdosproblems.com/196 - [DEGS77] Davis, J. A. and Entringer, R. C. and Graham, R. L. and Simmons, G. J., On permutations containing no long arithmetic progressions. Acta Arith. (1977), 81-90. - [Ho26] Ho, Boon Suan, A 4AP-free permutation of the positive integers. arXiv:2609.12780
Quoted from FormalConjectures/ErdosProblems/196.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/196.
The file states 1 research or textbook statement: 1 solved.
Erdos196.erdos_196
Solved: stated here; a Lean proof is at https://github.com/lkruer/conjectures/blob/8ede860e8fc90a300207a2c17e8aefe6167b3086/problems/erdos-196/lean/Erdos196.lean.
Must every permutation of \(\mathbb{N}\) contain a monotone 4-term arithmetic progression?
Here a monotone \(k\)-term arithmetic progression in a permutation \(f\) is a set of indices \(i_1 < \cdots < i_k\) such that \(f(i_1), \ldots, f(i_k)\) is an increasing or decreasing arithmetic progression. [DEGS77] showed that every permutation of \(\mathbb{N}\) contains a monotone 3-term arithmetic progression, and that there are permutations with no monotone 5-term arithmetic progression.
The answer is no: [Ho26] constructs an explicit permutation of the positive integers with no monotone 4-term arithmetic progression. Independent constructions with Lean formalizations were given shortly afterwards by Kruer and Kohlmeyer and, pseudonymously, in the repository
coleski/erdos196; the linked formal proof establishes the negation of this statement.
theorem erdos_196 : ¬ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP f 4
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/196.lean, line 50.
Sources
TheoremErdős Problem 197#
Reference: erdosproblems.com/197
Quoted from FormalConjectures/ErdosProblems/197.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/197.
The file states 1 research or textbook statement: 1 open.
Erdos197.erdos_197
Open: stated without proof.
Can \(\mathbb{N}\) be partitioned into two sets, each of which can be permuted to avoid monotone 3-term arithmetic progressions?
theorem erdos_197 :
∃ A B : Set ℕ, IsCompl A B ∧
(∃ f : ℕ ≃ A, ¬HasMonotoneAP (Subtype.val ∘ f) 3) ∧
(∃ g : ℕ ≃ B, ¬HasMonotoneAP (Subtype.val ∘ g) 3)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/197.lean, line 37.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.