LeanCat: A Lean Dataset for Evaluating Library-Grounded Category-Theoretic Reasoning

Modern formal theorem proving increasingly depends on large formal libraries, motivating focused evaluation datasets for library-grounded reasoning in addition to established olympiad-style, undergraduate, and other formal reasoning tasks. Category theory is a natural domain for this evaluation because proofs often rely on abstract interfaces, universal properties, and reusable library constructions. We introduce $\textbf{LeanCat}$, a compact evaluation dataset of 100 statement-level category-theory tasks in Lean 4 and Mathlib. Each task includes a natural-language statement, a Lean-checkable formal theorem file, topic and difficulty labels, and source metadata. LeanCat evaluates how models navigate Mathlib interfaces and compose existing abstractions, including tasks that require local definitions or bridge lemmas beyond direct theorem lookup. We evaluate strong generalist models, specialized provers, and retrieval-augmented proving protocols across separate settings. The best static generalist baseline solves 12/100 tasks under controlled pass@4 evaluation, while retrieve--generate--verify protocols reach 24/100 overall and 1/40 High tasks in the best controlled setting, highlighting how formal grounding, retrieval, and interaction change measured performance on this focused benchmark.