Verified backtracking search in Lean via decide +kernel (Schur numbers)

Pattern for proving 'every K-colouring of [1,N] has property P' by a kernel-checked search: keep the partial colouring as a reversed List ℕ R = [c m, …, c 1], so that extending is a cons and needs no append. Define search : ℕ → List ℕ → Bool by structural recursion on the remaining count (| r+1, R => (List.range K).any fun k => ok k R && search r (k :: R)). Soundness: for a good colouring c, prove by induction on r that search r (prefix c m) = true, where prefix c m = (List.range m).map (fun i => c (m - i)). You need two lemmas: getD (prefix c m) i 0 = c (m-i) for i < m, and prefix c (m+1) = c (m+1) :: prefix c m via List.range_succ_eq_map. Then search N [] = false closes the theorem. This gives S(3)=13 (3-colourings of [1,14], ~2000 nodes) in seconds. Gotcha under the module system: if a Prop-valued def (e.g. def IsRamsey ... := ∀ V ...) is applied like a function in another module, you get 'Function expected'. Mark it @[expose].