Add Erdős Problem 1171 (ω₁² multicolor partition)#3789
Add Erdős Problem 1171 (ω₁² multicolor partition)#3789henrykmichalewski wants to merge 2 commits intogoogle-deepmind:mainfrom
Conversation
Paul-Lez
left a comment
Paul-Lez
left a comment
There was a problem hiding this comment.
Thanks for the contribution! A few comments:
| **Status**: Proved under MA(countable) by Baumgartner [Ba89b]. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem baumgartner_under_MA : |
There was a problem hiding this comment.
Could we either remove this theorem for now, or replace True with a precise predicate for the form of Martin's Axiom being assumed? As written, True → ... does not record any extra set-theoretic assumption, so the declaration states the Baumgartner relation unconditionally. I think it would be better to keep this result in the docstring/TODO until the MA hypothesis has a faithful Lean predicate.
| **Status**: OPEN. | ||
| -/ | ||
| @[category research open, AMS 5] | ||
| theorem erdos_1171 : ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by |
There was a problem hiding this comment.
Could we state the open yes/no question using answer(sorry)?
Something like:
| theorem erdos_1171 : ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by | |
| theorem erdos_1171 : | |
| answer(sorry) ↔ | |
| ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k := by |
| /-! | ||
| # Erdős Problem 1171 | ||
|
|
||
| *Reference:* [erdosproblems.com/1171](https://www.erdosproblems.com/1171) |
There was a problem hiding this comment.
Could we include the original source [Va99, 7.84] in the module references? The Erdős page cites that as the source for this problem, and asks that original sources be used when referring to the problem.
| provides a witness for the `j`-color version. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem mono_k {j k : ℕ} (hjk : j ≤ k) |
There was a problem hiding this comment.
minor: I think this should be @[category API] rather than research solved, since it is local API about the new multicolor relation rather than a cited research result.
Paul-Lez
left a comment
Paul-Lez
left a comment
There was a problem hiding this comment.
One tiny follow-up nit:
| @@ -0,0 +1,167 @@ | |||
| /- | |||
| Copyright 2025 The Formal Conjectures Authors. | |||
There was a problem hiding this comment.
nit: since this is a new file in 2026, could you update the copyright year to 2026?
Per review on PR google-deepmind#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).
2 participants
Problem
Erdős Problem 1171: https://www.erdosproblems.com/1171
Multicolor partition relation concerning ω₁² and open questions about which partition relations hold.
Contents
OrdinalMultiColorRamsey α β γ kdefinition generalizing the binary ordinal partition relation tok+1colorsCloses #1993
Assisted by Claude (Anthropic).