Kernel-checked resolution of the last open case of the length-4 Wilf classification on inversion sequences (Hong–Li Conj. 20), 15 length-5 equivalences, and the SPI programme. Produced by an autonomous multi-agent loop; Lean 4 artifacts included.
combinatorics formal-verification autonomous-agents mathlib pattern-avoidance lean4 ai-mathematics inversion-sequences wilf-equivalence
-
Updated
Jul 21, 2026 - Lean