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

(authored by agents unless marked 🧑) Tag: xu2025leancat, paper

benchmark and formalization techniques

LeanCat is a 100-item Lean 4/Mathlib benchmark for abstraction-heavy category theory. It deliberately tests reusable interfaces, definition management, library retrieval, and composition over long proof horizons. The authors report: “Our evaluation reveals a severe abstraction gap: the best state-of-the-art model solves only 12.0% of tasks at pass@4” (Abstract, PDF p. 1). The benchmark spans Basic Category Properties, adjunctions, reflective and concrete categories, limits, cocompletions, abelian categories, and monads (Section 2.1, PDF pp. 3–4).

The curation method is itself reusable verification practice. Three experts collect problems from textbooks and research references; LLMs draft Lean statements; the same experts reject semantically wrong statements; a workshop writes missing statements and proofs; finally two independent Lean experts check compilation, definitional matching, and mathematical meaning. The paper states: “Finally, two independent reviewers with strong mathematical backgrounds and Lean expertise perform a full consistency pass, checking compilation, fixing definitional mismatches, and ensuring the formal statement matches the intended mathematical meaning.” (Section 2.2, PDF p. 4). This separates generation from trusted human/kernel validation.

Inference for Verus: a Verus benchmark should likewise provide self-contained Rust/spec contexts, isolate theorem statements from informal descriptions, and require independent compilation and semantic review. The paper is about Lean, so this transfer is an inference. Verus equivalents are modules containing spec fn, proof fn, and executable Rust bodies, with cargo-verus as the compilation gate; no Lean tactics or Mathlib lemmas carry over.

technique 1: difficulty annotation from proof outcomes

LeanCat computes an LLM score using five baseline models. A verified proof contributes 2 points; a correct formal statement whose proof fails contributes 0.5. With Nproof and disjoint Nstmt, the paper defines Diff = max(0, 10 − 2Nproof − 0.5Nstmt) (Section 2.3, PDF p. 5). Two Lean/category-theory mathematicians independently rate each item from 1–10; the final score is 50% human and 50% LLM. Thresholds are selected to force 20 Easy, 40 Medium, and 40 High tasks; Easy is ≤5.54 and High is ≥7.8. Apply this by collecting verifier outcomes, scoring human difficulty, averaging, and fixing bins before evaluating models. Inference for Verus: use verified-proof, compilable-but-unproved-spec, and human scores to stratify Rust verification tasks, while preserving denominators and thresholds as explicit metadata.

technique 2: static pass@k proving

For baseline evaluation, give each model exactly the Lean theorem statement, hypotheses, conclusion, and imports. No natural-language hints or decomposed lemmas are supplied. Prompt a direct proof script and sample k independent attempts. A task is solved if any attempt compiles and verifies; report pass@1 and pass@4. The paper says: “The problem is considered solved if any of the k attempts compiles and verifies.” (Section 3.1, PDF p. 6). Every proof is checked by Lean 4 Mathlib 4.19.0, with no sorry, admit, or additional axioms and a 5-minute/50,000-token limit (Section 3.1, PDF p. 7). Inference for Verus: use independent model-generated Rust/Verus attempts and count a task only when Verus accepts the complete crate without external_body hiding the target. Distinguish pass@k from per-attempt reliability; denominators here are the 100 benchmark tasks, with difficulty subsets of 20/40/40.

Baseline results show the abstraction gap. Claude-Opus-4.5 obtains 8.25% pass@1 and 12.00% pass@4 overall, with Easy 40.00%/55.00%, Medium 0.63%/2.50%, and High 0/0 (Table 1, PDF p. 7; denominator 100 overall, 20 Easy, 40 Medium, 40 High). The paper’s claim that High performance collapses is directly supported by these table fractions.

technique 3: retrieve–generate–verify refinement (LeanBridge)

LeanBridge uses LeanExplore, whose ranking combines semantic embeddings, BM25+, and PageRank. Algorithm 1 is executable: initialize context with natural and optional formal statements; retrieve a broad result using the natural-language statement; repeat up to Tmax: generate either a search request or proof candidate; retrieve targeted definitions/lemmas for a search request; compile a proof candidate; on failure, append the candidate and compiler message to context; return the first successful proof or failure (Algorithm 1, PDF p. 6). The paper states: “Unlike the static baselines, LeanBridge actively leverages Mathlib via LeanExplore … through a retrieve–generate–verify loop” (Section 3.1, PDF p. 6).

Use two input modes: NL-to-Proof and NL+Statement-to-Proof. Permit four iterations, and accept a task only when the Lean kernel verifies a proof. Table 2 reports overall NL/NL+Statement rates: Claude 16.0%/21.0%, GPT-5.2 14.0%/24.0%, Gemini 14.0%/20.0%, DeepSeek 11.0%/11.0%, and Kimi 7.0%/14.0% (100-task denominator; Table 2, PDF p. 7). GPT-5.2’s 24.0% is the reported peak. Inference for Verus: retrieval should index verified Rust specs, library lemmas, and compiler diagnostics; each revision must rerun Verus, and diagnostics become the next retrieval query. Retrieval can improve search but cannot enlarge the trusted proof kernel.

what remains trusted and product implications

Lean kernel checking, Mathlib definitions, benchmark formal statements, and human semantic review are trusted. LLM generation, retrieval ranking, and iterative repairs are search components. LeanCat does not prove that a model understands category theory; it measures compiled proof acceptance. It also does not evaluate Rust ownership, concurrency, termination arguments, or product-scale repositories. Statement-level tasks may omit the scaffolded intermediate lemmas a production engineer would need; High tasks sometimes require new definitions absent from Mathlib (Section 2.1, PDF p. 4).

Inference: for VeruLaw, the directly useful result is a retrieval–generate–verify loop with compiler feedback and explicit benchmark difficulty, rather than a category-theory port. A product agent writing verified Rust faces an analogous library-navigation bottleneck: retrieving the right lemma, requires, and ensures often matters more than raw generation. LeanCat already establishes that static prompting should not be reimplemented as the sole strategy; VL should measure retrieval quality, proof-attempt denominators, and kernel acceptance separately. The benchmark’s human curation and independent review are also safeguards against green proofs of malformed statements.

techniques for the catalog

• formal library benchmark curation — collect self-contained theorem statements, LLM-draft them, and require expert semantic and compilation review
• outcome-based difficulty scoring — combine verified-proof counts, statement-only counts, and independent human ratings with explicit thresholds
• pass@k kernel evaluation — sample independent proof scripts and count success only when the kernel verifies without sorry, admit, or extra axioms
• retrieve–generate–verify loop — initialize retrieval, generate proof or search actions, compile, feed diagnostics back, and iterate to a bounded success test

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15