feat(ErdosProblems): 15x ramsey theory formalizations#3588
feat(ErdosProblems): 15x ramsey theory formalizations#3588ryantuck wants to merge 9 commits intogoogle-deepmind:mainfrom
Conversation
|
Thanks! Some first remarks:
|
|
@mo271 thanks for the feedback! As advised, I had Opus 4.6 do the following (fine-grain markdown session logs included to show the work): 1 - 3c168fa consolidated reused definitions among my erdos contributions (session logs)
2 - 6b288cd also consolidated wikipedia Ramsey code for reuse (session logs)
3 - 45fd907 holistically assessed whether all Ramsey-related code was in an appropriate place or needed further consolidation, and clarified some references in the erdos file implementations (session logs)
|
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Please extend my comments accordingly to the other problems
| /-- | ||
| Erdős Problem 1014 [Er71, p.99]: | ||
|
|
||
| For fixed $k \geq 3$, | ||
| $$\lim_{l \to \infty} R(k, l+1) / R(k, l) = 1,$$ | ||
| where $R(k, l)$ is the Ramsey number. | ||
|
|
||
| Formulated as: for every $\varepsilon > 0$, there exists $L_0$ such that for all $l \geq L_0$, | ||
| $|R(k, l+1) / R(k, l) - 1| \leq \varepsilon$. | ||
| -/ | ||
| @[category research open, AMS 5] | ||
| theorem erdos_1014 (k : ℕ) (hk : k ≥ 3) : |
There was a problem hiding this comment.
Can you state the k = 3 separately since it already is open?
There was a problem hiding this comment.
And also perhaps a statement of category undergraduate for the case k=2?
/--
The k=2 case: R(2, l+1)/R(2, l) → 1, since R(2, l) = l for all l.
This follows from the fact that for any graph G on n vertices, either G has an edge
(a 2-clique) or G = ⊥ and Gᶜ = ⊤ contains an l-clique (when l ≤ n).
-/
@[category undergraduate, AMS 5]
theorem erdos_1014_k_eq_2 :
Tendsto (fun l : ℕ =>
(graphRamseyNumber 2 (l + 1) : ℝ) / (graphRamseyNumber 2 l : ℝ))
atTop (nhds 1) := by
simp_rw [graphRamseyNumber_two]
suffices h : Tendsto (fun l : ℕ => (1 : ℝ) / (l : ℝ)) atTop (nhds 0) by
have := tendsto_const_nhds (x := (1 : ℝ)).add h
simp only [add_zero] at this
apply this.congr'
filter_upwards [Ici_mem_atTop 1] with l (hl : 1 ≤ l)
have : (l : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
push_cast; field_simp
exact (tendsto_inv_atTop_zero (𝕜 := ℝ)).comp tendsto_natCast_atTop_atTop
|>.congr fun n => (one_div (n : ℝ)).symm
This works together with graphRamseyNumber_two suggested below in Ramsey.lean
|
|
||
| *Reference:* [erdosproblems.com/1014](https://www.erdosproblems.com/1014) | ||
|
|
||
| [Er71] Erdős, P., _Topics in combinatorial analysis_, pp. 95-99, 1971. |
There was a problem hiding this comment.
The article seems to only be 19 pages long. Please check all references!
|
|
||
| *Reference:* [erdosproblems.com/1030](https://www.erdosproblems.com/1030) | ||
|
|
||
| If $R(k,l)$ is the Ramsey number then prove the existence of some $c > 0$ such that |
There was a problem hiding this comment.
Agree this is odd phrasing but is coming directly from the source website: https://www.erdosproblems.com/1030
I've submitted a comment there on the problem to suggest an edit:
The way this problem is phrased could probably be improved ("the Ramsey number"?) and it appears the limit needs defining (is that k -> infinity?). I don't have access to the source but am working on contributing a formalization at #3588 and this was raised as an issue :)
| See also problems [544](https://www.erdosproblems.com/544) and | ||
| [1014](https://www.erdosproblems.com/1014). | ||
|
|
||
| OEIS: [A000791](https://oeis.org/A000791), [A059442](https://oeis.org/A059442). |
There was a problem hiding this comment.
What's the relevance of the first one?
There was a problem hiding this comment.
https://www.erdosproblems.com/1030 lists these two sequences as relevant which is why it's listed here.
It appears that 544 is marked as relevant since it describes R(3,k), and that OEIS sequence is listed as the relevant one.
YaelDillies
added
the
awaiting-author
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Partial review first 5/15.
Some issues are similar in each
module docstring shouldn't repeat what is later mentioned in theorem docstrings and Reference should be organized with bullet points like is done in other files in this repo.
Also let's always add a --TODO for the remaining variants in the additional material if not all of them are formalised here.
| @[category research open, AMS 5] | ||
| theorem ramsey_number_five_five : | ||
| R(5, 5) = answer(sorry) := by | ||
| sorry |
There was a problem hiding this comment.
not really related to that pull request, but since it is nearby
answer(sorry) ↔ 43 < R(5, 5) and
``answer(sorry) ↔ R(5, 5) < 46`
as new research open statements, to capture the easiest open cases here.
(no worry if you don't add it, I will do it later if it is not done here..)
| /-- The classical diagonal Ramsey number `R(k) := R(K_k, K_k)`. -/ | ||
| noncomputable def diagRamseyNumber (k : ℕ) : ℕ := | ||
| ramseyNumber (⊤ : SimpleGraph (Fin k)) | ||
|
|
There was a problem hiding this comment.
| /-- The two Ramsey number definitions agree on the diagonal -/ | |
| theorem graphRamseyNumber_self_eq_diagRamseyNumber (k : ℕ) : | |
| graphRamseyNumber k k = diagRamseyNumber k := by | |
| unfold graphRamseyNumber diagRamseyNumber ramseyNumber IsGraphRamsey | |
| congr 1; ext n; simp only [Set.mem_setOf_eq, not_and_or] | |
| exact forall_congr' fun G => or_congr | |
| (by rw [← not_free, ← cliqueFree_iff_top_free]; simp [Fintype.card_fin]) | |
| (by rw [← not_free, ← cliqueFree_iff_top_free]; simp [Fintype.card_fin]) | |
Let's add a test statement like this, which would also probably be useful in proofs
| /-- The classical diagonal Ramsey number `R(k) := R(K_k, K_k)`. -/ | ||
| noncomputable def diagRamseyNumber (k : ℕ) : ℕ := | ||
| ramseyNumber (⊤ : SimpleGraph (Fin k)) | ||
|
|
There was a problem hiding this comment.
| /-- The two Ramsey number definitions agree on the diagonal -/ | |
| theorem graphRamseyNumber_self_eq_diagRamseyNumber (k : ℕ) : | |
| graphRamseyNumber k k = diagRamseyNumber k := by | |
| unfold graphRamseyNumber diagRamseyNumber ramseyNumber IsGraphRamsey | |
| congr 1; ext n; simp only [Set.mem_setOf_eq, not_and_or] | |
| exact forall_congr' fun G => or_congr | |
| (by rw [← not_free, ← cliqueFree_iff_top_free]; simp [Fintype.card_fin]) | |
| (by rw [← not_free, ← cliqueFree_iff_top_free]; simp [Fintype.card_fin]) | |
Let's add a test statement like this, which would also probably be useful in proofs
| /-- | ||
| Erdős Problem 1014 [Er71, p.99]: | ||
|
|
||
| For fixed $k \geq 3$, | ||
| $$\lim_{l \to \infty} R(k, l+1) / R(k, l) = 1,$$ | ||
| where $R(k, l)$ is the Ramsey number. | ||
|
|
||
| Formulated as: for every $\varepsilon > 0$, there exists $L_0$ such that for all $l \geq L_0$, | ||
| $|R(k, l+1) / R(k, l) - 1| \leq \varepsilon$. | ||
| -/ | ||
| @[category research open, AMS 5] | ||
| theorem erdos_1014 (k : ℕ) (hk : k ≥ 3) : |
There was a problem hiding this comment.
And also perhaps a statement of category undergraduate for the case k=2?
/--
The k=2 case: R(2, l+1)/R(2, l) → 1, since R(2, l) = l for all l.
This follows from the fact that for any graph G on n vertices, either G has an edge
(a 2-clique) or G = ⊥ and Gᶜ = ⊤ contains an l-clique (when l ≤ n).
-/
@[category undergraduate, AMS 5]
theorem erdos_1014_k_eq_2 :
Tendsto (fun l : ℕ =>
(graphRamseyNumber 2 (l + 1) : ℝ) / (graphRamseyNumber 2 l : ℝ))
atTop (nhds 1) := by
simp_rw [graphRamseyNumber_two]
suffices h : Tendsto (fun l : ℕ => (1 : ℝ) / (l : ℝ)) atTop (nhds 0) by
have := tendsto_const_nhds (x := (1 : ℝ)).add h
simp only [add_zero] at this
apply this.congr'
filter_upwards [Ici_mem_atTop 1] with l (hl : 1 ≤ l)
have : (l : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
push_cast; field_simp
exact (tendsto_inv_atTop_zero (𝕜 := ℝ)).comp tendsto_natCast_atTop_atTop
|>.congr fun n => (one_div (n : ℝ)).symm
This works together with graphRamseyNumber_two suggested below in Ramsey.lean
| noncomputable def diagRamseyNumber (k : ℕ) : ℕ := | ||
| ramseyNumber (⊤ : SimpleGraph (Fin k)) | ||
|
|
||
| end SimpleGraph |
There was a problem hiding this comment.
and some more basic statements like this
| end SimpleGraph | |
| /-- `IsGraphRamsey n 2 l` holds iff `l ≤ n`: any graph on `n ≥ l` vertices either has | |
| an edge (a 2-clique) or is edgeless (so its complement ⊤ has an `l`-clique). -/ | |
| theorem isGraphRamsey_two_iff {n l : ℕ} : | |
| IsGraphRamsey n 2 l ↔ l ≤ n := by | |
| constructor | |
| · intro h | |
| by_contra hlt | |
| push_neg at hlt | |
| exact h ⊥ ⟨cliqueFree_bot le_rfl, | |
| by rw [compl_bot]; exact cliqueFree_of_card_lt (by simp [Fintype.card_fin]; omega)⟩ | |
| · intro hle G | |
| rw [not_and_or] | |
| by_cases hG : G.CliqueFree 2 | |
| · right; rw [cliqueFree_two.mp hG, compl_bot] | |
| intro hcf | |
| have : ¬ (⊤ : SimpleGraph (Fin n)).CliqueFree n := by | |
| have := not_cliqueFree_card_of_top_embedding (α := Fin n) (RelEmbedding.refl _) | |
| simpa [Fintype.card_fin] using this | |
| exact this (hcf.mono hle) | |
| · exact Or.inl hG | |
| /-- `R(2, l) = l` for all `l`. -/ | |
| theorem graphRamseyNumber_two (l : ℕ) : graphRamseyNumber 2 l = l := by | |
| apply le_antisymm | |
| · exact Nat.sInf_le (isGraphRamsey_two_iff.mpr le_rfl) | |
| · exact le_csInf ⟨l, isGraphRamsey_two_iff.mpr le_rfl⟩ | |
| fun n hn => isGraphRamsey_two_iff.mp hn | |
| end SimpleGraph |
| theorem erdos_112 : | ||
| ∀ n m : ℕ, 2 ≤ n → 2 ≤ m → | ||
| dirRamseyNum n m = answer(sorry) := by |
There was a problem hiding this comment.
Please also add the smallest open cases here!
| to a 3-coloring. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem erdos_112.variants.ramsey_sandwich : |
There was a problem hiding this comment.
There is something wrong here: AlphaProof could disprove the statment!
@[category research solved, AMS 5]
theorem erdos_112.variants.ramsey_sandwich :
¬ (∀ n m : ℕ, 2 ≤ n → 2 ≤ m →
graphRamseyNum n m ≤ dirRamseyNum n m ∧
dirRamseyNum n m ≤ graphRamseyNum3 n m m) := by
-- AlphaProof found a disproof
push_neg
delta graphRamseyNum3 graphRamseyNum dirRamseyNum
use 2,2
rw[{s |_}.eq_empty_of_subset_empty]
· use refl _,refl _, fun and=>?_
rw[{s |_}.eq_empty_of_subset_empty]
· rewrite[Nat.sInf_empty,Nat.lt_iff_add_one_le,le_csInf_iff]
· exact (fun a s=>a.pos_of_ne_zero (by cases. with cases(s) PEmpty rfl (by repeat use default) with use (by valid:).elim (·.eq_empty_of_isEmpty▸nofun)))
· bound
use 3,fun _ _ _ a=>?_
rcases a
delta Erdos112.Digraph.IsTransTournament Erdos112.Digraph.IsIndepSet
by_cases h:∃ R M,R≠M∧‹∀ R M,Prop› R M
· simp_rw [ Fintype.bijective_iff_injective_and_card]
let⟨x,y,z,w⟩ :=h
classical use Or.inr ⟨ _, Finset.card_pair z, (if ·.1=0 then⟨x,by bound⟩else⟨y,by bound⟩),?_⟩
simp_all[Function.Injective,z.symm,Fin.forall_iff]
use fun and Y A B=>match A,and with|0,0|0,1|1,0|1,1=>by grind,fun A B R L=>by match A,R with|0,0|0,1|1,0|1,1=>grind
· exact (.inl (( Finset.exists_subset_card_eq (le_of_lt (Eq.ge (by assumption)))).imp fun and=>.symm ∘.imp_left fun and _ _ _ _ A=>h ⟨ _, _, fun and=>by simp_all only, A⟩))
· use fun and f=>match f (if.<. then(0)else 1) with|.inl ⟨x,A, B⟩|.inr<|.inl ⟨x,A, B⟩|.inr<|.inr ⟨x,A, B⟩=>(Finset.one_lt_card.1 A.ge).elim (by grind)
· use fun and f=>by cases f (.<.) with use (by valid:).elim fun and x =>( Finset.one_lt_card.1 x.1.ge).elim fun and⟨i,A, B, M⟩=>absurd (x.2 and i A B) (absurd (x.2 A B and i) ∘by grind)The bug could be about the missing symmetry condition flagged above?!
| /-- An $r$-edge-coloring of the complete graph $K_N$: a function that assigns a | ||
| color in $\operatorname{Fin} r$ to each ordered pair of vertices. | ||
| Note: this allows coloring of self-loops ($\chi\, x\, x$), which is semantically | ||
| meaningless for $K_N$ but harmless since `IsMonoKkFree` only examines pairs | ||
| with $x \ne y$. -/ | ||
| def EdgeColoring (N r : ℕ) : Type := Fin N → Fin N → Fin r | ||
|
|
||
| /-- A vertex set $S$ is monochromatic-$K_k$-free in color $c$ under coloring $\chi$ if | ||
| there is no $k$-element subset of $S$ in which every pair of distinct vertices | ||
| receives color $c$. -/ | ||
| def IsMonoKkFree {N r : ℕ} (χ : EdgeColoring N r) (c : Fin r) | ||
| (k : ℕ) (S : Finset (Fin N)) : Prop := | ||
| ∀ T : Finset (Fin N), T ⊆ S → T.card = k → | ||
| ∃ x ∈ T, ∃ y ∈ T, x ≠ y ∧ χ x y ≠ c | ||
|
|
||
| /-- The generalized Ramsey number $R(n; k, r)$: the smallest $N$ such that for | ||
| every symmetric $r$-coloring of the edges of $K_N$ (i.e., $\chi\, x\, y = \chi\, y\, x$), | ||
| there exists a set of $n$ vertices and a color $c$ such that the set is | ||
| $K_k$-free in color $c$. -/ | ||
| noncomputable def multicolorRamseyNum (n k r : ℕ) : ℕ := | ||
| sInf {N : ℕ | ∀ (χ : EdgeColoring N r), (∀ x y, χ x y = χ y x) → | ||
| ∃ (S : Finset (Fin N)) (c : Fin r), | ||
| S.card = n ∧ IsMonoKkFree χ c k S} |
There was a problem hiding this comment.
are those definition also needed in other Erdős problems? if so --> move to ForMathlib.
| The status of this generalized conjecture is unclear given the issues with | ||
| the $k = 3$ upper bound. | ||
| -/ | ||
| @[category research open, AMS 5] |
There was a problem hiding this comment.
Isn't it that here the status is known to false, so the negation of the statment is solved? I don't quite know what make of it from the review comments
At least as written the statement doesn't make much sense, AlphaProof gives a simple disproof:
theorem erdos_129_general_bounds :
¬ (∀ r : ℕ, 2 ≤ r → ∀ k : ℕ, 2 ≤ k →
∃ C₁ C₂ : ℝ, 1 < C₁ ∧ 1 < C₂ ∧
∀ n : ℕ, C₁ ^ (n : ℝ) ^ ((1 : ℝ) / ((k : ℝ) - 1))
< (multicolorRamseyNum n k r : ℝ)
∧ (multicolorRamseyNum n k r : ℝ)
< C₂ ^ (n : ℝ) ^ ((1 : ℝ) / ((k : ℝ) - 1))) := by
push_neg
refine ⟨2,refl _,2,refl _,fun _ _ _ _=> ⟨0,.trans (by (norm_num)) ∘le_of_lt⟩⟩| for all positive integers $n$. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem erdos_129_lower_bound : |
There was a problem hiding this comment.
This claims the lower bound for all n, including n=0,1,2. For small n, multicolorRamseyNum n 3 r could be 0 (or very small), while C^√n with C > 1 is at least 1. This is likely trivially false for n=0 since multicolorRamseyNum 0 3 r = 0 but C^0 = 1 > 0. Should perahps use ∀ᶠ n in atTop or add 1 ≤ n or something like that.
And checking with AlphaProof indeed gives a disproof:
theorem erdos_129_lower_bound :
¬ (∀ r : ℕ, 1 ≤ r →
∃ C : ℝ, 1 < C ∧
∀ n : ℕ, C ^ Real.sqrt (n : ℝ) < (multicolorRamseyNum n 3 r : ℝ)) := by
push_neg
delta multicolorRamseyNum
delta IsMonoKkFree EdgeColoring Real.sqrt
exact ⟨1,refl _,fun A B=>⟨0,.trans (mod_cast csInf_le' fun and i=>⟨{},0,rfl, by aesop⟩) ( A.rpow_nonneg (one_pos.trans B).le _)⟩⟩
Library (FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Ramsey.lean): - Added `graphRamseyNumber_self_eq_diagRamseyNumber` theorem (diagonal agreement) - Added `isGraphRamsey_two_iff` and `graphRamseyNumber_two` (R(2,l) = l) RamseyNumbers.lean: - Added R(5,5) open case statements: `43 < R(5,5)` and `R(5,5) < 46` 112.lean: - Trimmed module docstring, reformatted references as bullet points - Fixed `graphRamseyNum` and `graphRamseyNum3` to require symmetric colorings - Fixed `erdos_112` answer format to `(answer(sorry) : ℕ → ℕ → ℕ) n m` - Added smallest open cases: `k(3,3)` and `k(3,4)` - Added `-- TODO` for remaining variants 129.lean: - Trimmed module docstring, reformatted references - Fixed `erdos_129_lower_bound`: added `1 ≤ n` guard - Fixed `erdos_129_general_bounds`: changed `∀ n` to `∀ᶠ n in atTop` 1014.lean: - Trimmed module docstring, reformatted references - Added `erdos_1014.variants.k_eq_3` (open, k=3 case) - Added `erdos_1014.variants.k_eq_2` (undergraduate, k=2 case) 1030.lean: - Trimmed module docstring, reformatted references - Renamed `erdos_1030_weak` → `erdos_1030.variants.weak` - Added `-- TODO` for Burr–Erdős–Faudree–Schelp bound All 15 files: - Reformatted references to bullet-point style - Trimmed module docstrings to avoid repeating theorem content - Added `-- TODO` markers for unformalised variants
3 participants
Followup to #3422. Contains 15x formalizations for open problems relating to Ramsey theory.
Problems: