LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

Author: Xu, Rongge; Dai, Hui; Fu, Yiming; Jiang, Jiedong; Nie, Tianjiao; Wang, Hongwei; Wang, Junkai; Yang, Holiverse; Yang, Jiatong; Zhang, Zhi-Hao.
[Equal contributions; authors listed by surname.]

Published in arXiv (preprint), 2025

Summary: First Lean benchmark dedicated to formal category theory: Statement-level Lean tasks across 8 clusters (e.g., adjunctions, limits-colimits, abelian categories, monads) to stress-test abstraction-heavy, library-mediated reasoning; tough baselines (8.25% pass@1 / 12.00% pass@4) expose the natural-to-formal bottleneck, and LeanBridge + Lean-Explore (retrieve-generate-verify with compiler feedback) improves performance on a subset.