From b7fb6dbc4df448fa3d703b5c3341939e8a1926d2 Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Fri, 17 Apr 2026 09:25:07 +0100 Subject: [PATCH 1/3] =?UTF-8?q?feat(ErdosProblems/1171):=20formalize=20?= =?UTF-8?q?=CF=89=E2=82=81=C2=B2=20multicolor=20partition=20relation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- FormalConjectures/ErdosProblems/1171.lean | 167 ++++++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/1171.lean diff --git a/FormalConjectures/ErdosProblems/1171.lean b/FormalConjectures/ErdosProblems/1171.lean new file mode 100644 index 0000000000..9906a2f473 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1171.lean @@ -0,0 +1,167 @@ +/- +Copyright 2025 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1171 + +*Reference:* [erdosproblems.com/1171](https://www.erdosproblems.com/1171) + +*References for known results:* +- [EH74] Erdős, Paul and Hajnal, András, Unsolved and solved problems in set theory. Proceedings + of the Tarski symposium (1974), 269-287. +- [Ba89b] Baumgartner, James E., Partition relations for countable topological spaces. J. Combin. + Theory Ser. A (1986), 38-54. + +## Problem Statement + +Is it true that, for all finite $k$ (with $k < \omega$), +$$\omega_1^2 \to (\omega_1 \cdot \omega, \underbrace{3, \ldots, 3}_{k})^2_{k+1}?$$ + +This is a multicolor generalization of the Erdős–Hajnal theorem. It asks whether every +$(k+1)$-coloring of the pairs (edges) of the complete graph on $\omega_1^2$ either: +- produces a monochromatic set of order type $\omega_1 \cdot \omega$ in color 0, or +- produces a monochromatic triangle $K_3$ in some non-zero color $i \in \{1, \ldots, k\}$. + +## Known Results + +- **Erdős–Hajnal** [EH74]: $\omega_1^2 \to (\omega_1 \cdot \omega, 3)^2$ (the $k = 1$ case). + This is the binary partition relation with one "large" color and one "triangle" color. +- **Baumgartner** [Ba89b]: Under a form of Martin's axiom (MA), the binary relation + $\omega_1 \cdot \omega \to (\omega_1 \cdot \omega, 3)^2$ holds. + +## Overview + +The key novelty here is `OrdinalMultiColorRamsey`: a $(k+1)$-color generalization of the +binary ordinal Ramsey relation. In `OrdinalMultiColorRamsey α β γ k`: +- `α` is the ordinal whose pairs are colored (the vertex set), +- `β` is the ordinal type required for a color-0 clique, +- `γ` is the clique size (as a cardinal) required for each non-zero color, +- `k` is the number of non-zero colors (so there are `k+1` colors total). + +The open question `erdos_1171` asks whether this holds for all finite `k` with +`α = ω₁²`, `β = ω₁ · ω`, `γ = 3`. +-/ + +open Cardinal Ordinal SimpleGraph + +namespace Erdos1171 + +universe u + +/- ### The multicolor ordinal partition relation -/ + +/-- +`OrdinalMultiColorRamsey α β γ k` asserts the multicolor partition relation +`α → (β, γ, γ, …, γ)²_{k+1}` (with `k` copies of `γ`). + +It states: for any function `col : Sym2 α.ToType → Fin (k + 1)` assigning one of `k+1` colors +to each pair from `α`, one of the following holds: +* Color 0: there is a set `s ⊆ α.ToType` of order type `β` that is monochromatic in color 0 + (i.e. every pair in `s` gets color 0), or +* Color i (for some `i : Fin k`): there is a set `s ⊆ α.ToType` with `#s = γ` that is + monochromatic in color `i.succ` (i.e. every pair in `s` gets color `i.succ`). + +When `k = 1` this reduces to the binary partition relation `α → (β, γ)²`. +-/ +def OrdinalMultiColorRamsey (α β : Ordinal.{u}) (γ : Cardinal.{u}) (k : ℕ) : Prop := + ∀ col : Sym2 α.ToType → Fin (k + 1), + -- Either color-0 clique of order type β ... + (∃ s : Set α.ToType, + (∀ x ∈ s, ∀ y ∈ s, x ≠ y → col s(x, y) = 0) ∧ + typeLT s = β) ∨ + -- ... or for some non-zero color i, a clique of cardinality γ. + (∃ (i : Fin k) (s : Set α.ToType), + (∀ x ∈ s, ∀ y ∈ s, x ≠ y → col s(x, y) = i.succ) ∧ + #s = γ) + +/- ### The main open problem -/ + +/-- +**OPEN**: Is it true that for all finite $k < \omega$, +$$\omega_1^2 \to (\omega_1 \cdot \omega, \underbrace{3, \ldots, 3}_{k})^2_{k+1}?$$ + +In any $(k+1)$-coloring of the pairs of the complete graph on $\omega_1^2$, either: +* there is a color-0 set of order type $\omega_1 \cdot \omega$, or +* there is a monochromatic triangle $K_3$ in some non-zero color. + +The case $k = 1$ (binary, `erdos_1171.variants.k_one`) is the Erdős–Hajnal theorem. + +**Status**: OPEN. +-/ +@[category research open, AMS 5] +theorem erdos_1171 : ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by + sorry + +/- ### Variants and known results -/ + +namespace erdos_1171.variants + +/-- +**Erdős–Hajnal theorem**: The case $k = 1$. + +$\omega_1^2 \to (\omega_1 \cdot \omega, 3)^2$: in any 2-coloring of the pairs of $K_{\omega_1^2}$, +there is either a color-0 set of order type $\omega_1 \cdot \omega$, or a color-1 triangle. + +This is the binary Ramsey relation `OrdinalRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3`, which can be +seen as the $k = 1$ instance of `OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 1`. + +**Status**: Proved (Erdős–Hajnal [EH74]). +-/ +@[category research solved, AMS 5] +theorem k_one : OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 1 := by + sorry + +/-- +**Reduction**: `OrdinalMultiColorRamsey` is monotone in the number of non-zero colors. + +If the `k`-color version `OrdinalMultiColorRamsey α β γ k` holds, then the `j`-color version +holds for all `j ≤ k`. A `j+1`-coloring can be embedded into a `k+1`-coloring by composing +with the inclusion `Fin (j+1) ↪ Fin (k+1)`, so a witness for the `k`-color version +provides a witness for the `j`-color version. +-/ +@[category research solved, AMS 5] +theorem mono_k {j k : ℕ} (hjk : j ≤ k) + (hk : OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k) : + OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 j := by + sorry + +/-- +**Baumgartner under MA**: Assuming a form of Martin's Axiom, the binary partition relation +$\omega_1 \cdot \omega \to (\omega_1 \cdot \omega, 3)^2$ holds. + +Baumgartner [Ba89b] proved that under MA(countable), the order type $\omega_1 \cdot \omega$ +itself has the self-similar Ramsey property with triangles. This is the $k = 1$ case +with $\alpha = \omega_1 \cdot \omega$ (rather than $\omega_1^2$). + +This provides evidence toward `erdos_1171` by establishing a Ramsey-type property at +the "target" order type. + +**Status**: Proved under MA(countable) by Baumgartner [Ba89b]. +-/ +@[category research solved, AMS 5] +theorem baumgartner_under_MA : + -- MA(countable) placeholder: in this formalization we take it as a hypothesis. + -- The actual statement of MA(countable) involves a forcing axiom for c.c.c. posets. + True → + OrdinalMultiColorRamsey (ω_ 1 * ω) (ω_ 1 * ω) 3 1 := by + intro _hMA + sorry + +end erdos_1171.variants + +end Erdos1171 From 06eaf8841040cce8ed7f766cd4d2e1a599f0d0aa Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Sun, 19 Apr 2026 10:57:55 +0100 Subject: [PATCH 2/3] Address Paul-Lez review: 5 fixes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per review on PR #3789: - Copyright year → 2026 - Add [Va99, 7.84] reference per Erdős citation policy - Use `answer(sorry) ↔` pattern for the open main theorem - Change `mono_k` category from `research solved` to `API` (local lemma) - Remove `baumgartner_under_MA` theorem — `True → …` was vacuous. Replaced with a block comment documenting the result as deferred until a faithful Lean predicate for Martin's Axiom is available. Assisted by Claude (Anthropic). --- FormalConjectures/ErdosProblems/1171.lean | 35 +++++++---------------- 1 file changed, 11 insertions(+), 24 deletions(-) diff --git a/FormalConjectures/ErdosProblems/1171.lean b/FormalConjectures/ErdosProblems/1171.lean index 9906a2f473..0adf4c868d 100644 --- a/FormalConjectures/ErdosProblems/1171.lean +++ b/FormalConjectures/ErdosProblems/1171.lean @@ -1,5 +1,5 @@ /- -Copyright 2025 The Formal Conjectures Authors. +Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. @@ -22,6 +22,7 @@ import FormalConjectures.Util.ProblemImports *Reference:* [erdosproblems.com/1171](https://www.erdosproblems.com/1171) *References for known results:* +- [Va99, 7.84] Vardi, Menachem, *Partition Relations, Problem Collection*, available online. - [EH74] Erdős, Paul and Hajnal, András, Unsolved and solved problems in set theory. Proceedings of the Tarski symposium (1974), 269-287. - [Ba89b] Baumgartner, James E., Partition relations for countable topological spaces. J. Combin. @@ -104,7 +105,9 @@ The case $k = 1$ (binary, `erdos_1171.variants.k_one`) is the Erdős–Hajnal th **Status**: OPEN. -/ @[category research open, AMS 5] -theorem erdos_1171 : ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by +theorem erdos_1171 : + answer(sorry) ↔ + ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by sorry /- ### Variants and known results -/ @@ -134,33 +137,17 @@ holds for all `j ≤ k`. A `j+1`-coloring can be embedded into a `k+1`-coloring with the inclusion `Fin (j+1) ↪ Fin (k+1)`, so a witness for the `k`-color version provides a witness for the `j`-color version. -/ -@[category research solved, AMS 5] +@[category API, AMS 5] theorem mono_k {j k : ℕ} (hjk : j ≤ k) (hk : OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k) : OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 j := by sorry -/-- -**Baumgartner under MA**: Assuming a form of Martin's Axiom, the binary partition relation -$\omega_1 \cdot \omega \to (\omega_1 \cdot \omega, 3)^2$ holds. - -Baumgartner [Ba89b] proved that under MA(countable), the order type $\omega_1 \cdot \omega$ -itself has the self-similar Ramsey property with triangles. This is the $k = 1$ case -with $\alpha = \omega_1 \cdot \omega$ (rather than $\omega_1^2$). - -This provides evidence toward `erdos_1171` by establishing a Ramsey-type property at -the "target" order type. - -**Status**: Proved under MA(countable) by Baumgartner [Ba89b]. --/ -@[category research solved, AMS 5] -theorem baumgartner_under_MA : - -- MA(countable) placeholder: in this formalization we take it as a hypothesis. - -- The actual statement of MA(countable) involves a forcing axiom for c.c.c. posets. - True → - OrdinalMultiColorRamsey (ω_ 1 * ω) (ω_ 1 * ω) 3 1 := by - intro _hMA - sorry +/- **Baumgartner under MA (currently deferred)**: Assuming a form of Martin's Axiom, +the binary partition relation `ω₁·ω → (ω₁·ω, 3)²` holds [Ba89b]. We omit the Lean +statement for now because faithfully encoding the exact form of MA requires more work; +stating the result as `True → ...` would effectively make it unconditional. To be +restored once an appropriate MA predicate is available in the formalization. -/ end erdos_1171.variants From 4cff61d9d7d9df154c8fa9c4de686da035bae33b Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Wed, 22 Apr 2026 14:43:32 +0100 Subject: [PATCH 3/3] docs: add verbatim source statement to module docstring Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff. --- FormalConjectures/ErdosProblems/1171.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/FormalConjectures/ErdosProblems/1171.lean b/FormalConjectures/ErdosProblems/1171.lean index 0adf4c868d..bd4ac17338 100644 --- a/FormalConjectures/ErdosProblems/1171.lean +++ b/FormalConjectures/ErdosProblems/1171.lean @@ -19,6 +19,14 @@ import FormalConjectures.Util.ProblemImports /-! # Erdős Problem 1171 +**Verbatim statement (Erdős #1171, status O):** +> Is it true that, for all finite $k<\omega$,\[\omega_1^2\to (\omega_1\omega, 3,\ldots,3)_{k+1}^2?\] + +**Source:** https://www.erdosproblems.com/1171 + +**Notes:** OPEN + + *Reference:* [erdosproblems.com/1171](https://www.erdosproblems.com/1171) *References for known results:*