Definition of Schur numbers

Stream: mathlib4

[metakuntyyy]

Given this video https://www.youtube.com/watch?v=57V8Ud7PL8k from numberphile I wanted to define Schur numbers and prove that s 2 = 5. I have done the construction modulo boundedness for Nat.find. Is this worthy to be in mathlib? It seems that there is little combinatorics. I couldn't find Ramsey numbers and I need R(k,k,k) to complete the proof.

[metakuntyyy]

Here is the code. Suggestions welcome. Also who wants to guess what my favourite tactic is?

import Mathlib

def isSchurSolutionIjk {m: ℕ} (n i j k :ℕ) (f: ℕ → (Fin m)) :=
  i∈ Set.Icc 1 n ∧ j ∈ Set.Icc 1 n ∧ k ∈ Set.Icc 1 n ∧ i+j =k →
  f i ≠ f j ∨ f i ≠ f k ∨ f j ≠ f k

def isSchurSolution {m: ℕ} (n:ℕ) (f: ℕ → (Fin m)) :=
  ∀ i j k : Nat, isSchurSolutionIjk n i j k f



def schurSol : ℕ → Fin 2
  | 2 | 3 => 1
  | _ => 0

theorem ssol : isSchurSolution 4 schurSol :=by
  intro i j k h
  unfold schurSol
  have hlowi : 1 ≤ i:=by grind
  have hupi : i ≤ 4:=by grind
  have hlowj : 1 ≤ j:=by grind
  have hupj : j ≤ 4:=by grind
  have hlowk : 1 ≤ k:=by grind
  have hupk : k ≤ 4:=by grind
  interval_cases i
  all_goals interval_cases j
  all_goals interval_cases k
  repeat grind


def hasSchurSolution (n m : ℕ) := ∃ (f: ℕ → (Fin m)), isSchurSolution n f

theorem exists_noSchurSol00 : ¬ hasSchurSolution 0 0 := by
  intro ⟨ f, hf ⟩
  have x := (f 0).prop
  contradiction

theorem exists_nonSchurSol0  : ∃ n, ¬ hasSchurSolution n 0 := ⟨ 0 , exists_noSchurSol00⟩

theorem exists_nonSchurSol (m: ℕ) : ∃ n, ¬ hasSchurSolution n m := by
  have hh : m = 0 ∨ 0 < m := by grind
  rcases hh with h | h
  · rw[h]
    exact exists_nonSchurSol0
  ·
    sorry



open Classical in
noncomputable def schurNumber (m: ℕ) : ℕ :=
  Nat.find (exists_nonSchurSol m)

theorem hasSchurSolutionOneOne : hasSchurSolution 1 1 := by
  let f : ℕ → (Fin 1) := 0
  use f
  intro i j k h
  grind

theorem hasNoSchurSolutionTwoOne : ¬ hasSchurSolution 2 1 := by
  intro ⟨ f, hf ⟩
  have h0 : f = 0 := by grind
  have hc := hf 1 1 2
  unfold isSchurSolutionIjk at hc
  have hcc := hc ?_
  repeat grind


theorem hasSchurSolutionFourTwo : hasSchurSolution 4 2 :=
  ⟨ schurSol, ssol ⟩


theorem solEquiv {n m :ℕ } (f: ℕ → (Fin m)) (g: Equiv.Perm (Fin m )) (h: isSchurSolution n f) :
    isSchurSolution n (g ∘ f) := by
  unfold isSchurSolution at *
  unfold isSchurSolutionIjk at *
  intro i j k hcon
  have hg := h i j k hcon
  rcases hg with hc | hc | hc
  · left
    simpa
  · right
    left
    simpa
  · right
    right
    simpa


theorem hasNoSchurSolutionFiveTwo : ¬ hasSchurSolution 5 2 := by
  intro ⟨ f , h ⟩
  wlog h1 : f 1 = 0
  · exact this ((Equiv.swap 0 (f 1))∘ f) (solEquiv f (Equiv.swap 0 (f 1)) h) (by simp)
  have h2 : f 2 = 1 := by
    by_contra hc
    have hd := h 1 1 2
    unfold isSchurSolutionIjk at hd
    have he := hd (by grind)
    grind
  have h4 : f 4 = 0 := by
    by_contra hc
    have hd := h 2 2 4
    unfold isSchurSolutionIjk at hd
    have he := hd (by grind)
    grind
  have h3 : f 3 = 1 := by
    by_contra hc
    have hd := h 1 3 4
    unfold isSchurSolutionIjk at hd
    have he := hd (by grind)
    grind
  have h50 : f 5 = 0 := by
    by_contra hc
    have hd := h 2 3 5
    unfold isSchurSolutionIjk at hd
    have he := hd (by grind)
    grind
  have h51 : f 5 = 1 := by
    by_contra hc
    have hd := h 1 4 5
    unfold isSchurSolutionIjk at hd
    have he := hd (by grind)
    grind
  grind


theorem schurLe {l m n: ℕ} (h: hasSchurSolution n m) (hle : l ≤ n) : hasSchurSolution l m := by
  use h.choose
  intro i j k hi
  apply h.choose_spec
  grind




open Classical in
theorem schur0 : schurNumber 0 = 0 := by
  rw[schurNumber]
  rw[Nat.find_eq_zero]
  exact exists_noSchurSol00

open Classical in
theorem schur1 : schurNumber 1 = 2 := by
  rw[schurNumber]
  rw[Nat.find_eq_iff]
  constructor
  exact hasNoSchurSolutionTwoOne
  intro n h
  push_neg
  exact schurLe hasSchurSolutionOneOne (by grind)


open Classical in
theorem schur2 : schurNumber 2 = 5 := by
  rw[schurNumber]
  rw[Nat.find_eq_iff]
  constructor
  exact hasNoSchurSolutionFiveTwo
  intro n h
  push_neg
  exact schurLe hasSchurSolutionFourTwo (by grind)

[Snir Broshi]

Ramsey is being worked on here https://github.com/b-mehta/ExponentialRamsey/blob/master/ExponentialRamsey/Prereq/Ramsey.lean
AFAIK there's an effort to add it to Mathlib, starting with #30047

[metakuntyyy]

Ah, I see. Is it nevertheless worth making a PR with the partial results? All I think is missing is a proof of boundedness for all Schur numbers. Or should I wait until the Ramsey numbers are in Mathlib?

[Alfredo Moreira-Rosa]

Does anyone have an answer to the question i asked here related to schur numbers ?
https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Are.20Schur.20number.20compute.20NP.20hard/with/554181636

[Snir Broshi]

metakuntyyy said:

Ah, I see. Is it nevertheless worth making a PR with the partial results? All I think is missing is a proof of boundedness for all Schur numbers. Or should I wait until the Ramsey numbers are in Mathlib?

In general partial results are fine, but in this case you can't define the Schur numbers without the Ramsey proof, right? Mathlib doesn't accept code with sorry in it. Can you somehow avoid needing it?

Another option is to branch off from a PR that contains the Ramsey theory you need, and then list it as a dependency. But I'm not sure there's such a PR yet