A Complete Lean Formalization of a TCS Proving Benchmark

We formalize the public Phase 1 benchmark for Track 2 of the ICML 2026 AI for Math Workshop, Theoretical Computer Science Proving in Lean. The benchmark consists of 29 challenge files, totaling 500 points, and covers treaps, segment trees, binary heaps, Dijkstra's shortest-path algorithm, and Kruskal's minimum-spanning-tree algorithm. The submitted artifact checks in the supplied Lean 4.28.0, CSLib, and mathlib environment, with no remaining sorry or admit in the challenge files and no changes to the provided definition files. The development centers on abstraction relations and inductive invariants that connect executable data structures to their mathematical specifications: heap membership and priority invariants for Dijkstra, and a disjoint-set/forest connectivity invariant together with a cut-property exchange argument for Kruskal. We describe the proof organization and the library interfaces suggested by the development.