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 contains 100 category-theory tasks formalized in Lean 4 with Mathlib, organized into eight topic clusters: Basic Category Properties, Adjunctions, Reflective and Coreflective Subcategories, Concrete Categories, Limits and Colimits, Cocompletions, Abelian Categories, and Monads (Section 2.1, PDF p. 3; Appendix A, PDF p. 13). Its focus is library-grounded abstraction. 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, with performance collapsing from 55.0% on Easy tasks to 0.0% on High-difficulty tasks, highlighting a failure in compositional generalization.” (Abstract, PDF p. 1).
Three category-theory experts collect problems and review LLM-drafted statements. For statements the models cannot formalize correctly, a three-day workshop at Westlake University supplies statements and, when feasible, proofs. The final review checks compilation and mathematical meaning: “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). Tasks provide standalone theorem statements and necessary definitions; informal descriptions are stored in companion Markdown files. High-difficulty cases can require intermediate results absent from Mathlib (Section 2.1, PDF p. 3).
Inference: a Verus benchmark could reuse the separation between self-contained formal tasks, informal descriptions, compilation checks, and independent semantic review. The specific category-theory statements and Lean interfaces do not establish how well this would work for Rust verification.
technique 1: difficulty annotation from proof outcomes
Section 2.3 evaluates each problem using LeanBridge’s sequential refinement protocol across five baseline models. It assigns 2 points for a verified proof and 0.5 for a correct formal statement only when the proof fails. Its formula is Diff = max(0, 10 − 2Nproof − 0.5Nstmt), with disjoint proof and statement-only counts. Two mathematicians with Lean and category-theory expertise independently rate difficulty from 1–10. Human ratings receive 50% total weight, and the LLM score receives 50%. Thresholds enforce 20 Easy, 40 Medium, and 40 High tasks: Easy ≤5.54 and High ≥7.8 (Section 2.3, PDF p. 5).
The paper’s scoring descriptions conflict: the prose says “We assign 2 points for a full proof and 0.5 points for a correct statement (credited only if the proof fails).” (Section 2.3, PDF p. 5), but Appendix Figure 5 labels the statement weights 0.4, and Figures 5–6 contain LLM scores such as 9.6 (PDF pp. 15–16). Inference: the prose formula alone cannot reproduce those displayed scores; an implementation must resolve this discrepancy rather than silently choose a weight. For Verus, outcome-based difficulty and independent human ratings are candidate methods, not validated transfers.
technique 2: static pass@k proving
Baselines receive the Lean theorem statement, hypotheses, conclusion, and imports, without natural-language hints or decomposed lemmas. The prompt requests a complete proof script. For each task, sample k independent attempts: “The problem is considered solved if any of the k attempts compiles and verifies.” (Section 3.1, PDF p. 6). Generalist results report pass@1 and pass@4; Table 1 says pass@1 uses the unbiased estimator from Chen (2021) (PDF p. 7). Specialized provers receive pass@32 (Section 3.1, PDF p. 6; Table 3, PDF p. 8).
Verification uses Lean 4 with Mathlib v4.19.0. The acceptance rule is: “A proof is considered valid if the Lean kernel accepts it without errors and strictly contains no sorry, admit, or additional axiom declarations.” (Section 3.1, PDF p. 7). Each attempt has a 5-minute verification limit. Table 5 specifies temperature 1.0, a 50,000-token maximum for generalist models, and model-specific maxima for specialized provers (PDF p. 19), qualifying the generic 50,000-token limit stated in Section 3.1.
Claude-Opus-4.5 achieves 8.25% pass@1 and 12.00% pass@4 overall: Easy 40.00%/55.00%, Medium 0.63%/2.50%, and High 0.00%/0.00% (Table 1, PDF p. 7). Task counts are 100 overall and 20/40/40 by difficulty; pass@1 is an estimate over sampled attempts, not an integer count of tasks solved in one recorded run. The strongest specialized prover, DeepSeek-Prover-V2-671B, achieves 9.0% overall at pass@32, with 45.0% Easy and 0.0% Medium/High (Table 3, PDF p. 8).
Inference: an analogous Verus evaluation could sample independent proof attempts, require verifier acceptance, and report both task-level success within a sample budget and per-attempt reliability.
technique 3: retrieve–generate–verify refinement (LeanBridge)
LeanBridge retrieves Mathlib declarations through LeanExplore. The paper describes LeanExplore as using “a hybrid ranking strategy combining semantic embeddings, BM25+, and PageRank” (Section 3.1, PDF p. 6). Algorithm 1 is pseudocode: initialize context with the natural-language statement and optional formal statement; perform mandatory broad retrieval using the natural-language statement; then generate an action each iteration. A search request after the first iteration triggers retrieval and appends the request and results to context. A proof candidate is compiled; success returns the proof, while failure appends the candidate and compiler message. Exhausting the loop returns failure (Algorithm 1, PDF p. 6). The refinement prompt asks the model to analyze compiler errors and choose between a targeted search and corrected code (Appendix D.2, PDF p. 18).
The two input modes are NL-to-Proof and NL+Statement-to-Proof. The protocol allows at most four iterations, accepting a verified proof reached within that limit (Section 3.1, PDF p. 6); retrieval returns the top three results per query (Table 5, PDF p. 19). Successful NL-only candidates also receive human expert review for semantic alignment with the original problem (Section 3.1, PDF p. 7).
Table 2 reports overall NL-only/NL+Statement success rates: Claude-Opus-4.5 16.0%/21.0%, GPT-5.2 14.0%/24.0%, Gemini-3-Pro 14.0%/20.0%, DeepSeek-V3.2 11.0%/11.0%, and Kimi-K2 7.0%/14.0%, over 100 tasks (PDF p. 7). GPT-5.2’s 24.0% is the reported peak. Only GPT-5.2 and Gemini-3-Pro with NL+Statement solve a High task, both at 2.5% of 40 High tasks; Appendix E.1 identifies it as Problem 59 (PDF p. 19).
The Gemini-3-Pro ablation separates refinement from retrieval: overall success rises from 8.0% for static pass@4 to 12.0% for LeanBridge without search and 20.0% with search. Medium success is 5.0%/7.5%/17.5%, and High success is 0.0%/0.0%/2.5% (Table 4, Section 4.4, PDF pp. 9–10). Inference: these experiments support retrieval and compiler feedback for this setup; they do not establish that retrieval is necessary for every possible prover or domain.
Inference: a Verus agent could retrieve relevant specifications and proof lemmas, revise proofs using diagnostics, and rerun the verifier after each candidate. This paper does not test that transfer.
what remains trusted and product implications
Inference: kernel acceptance checks a proof against its formal statement; semantic review checks whether that statement represents the intended problem. Both matter when a model generates the formalization. The paper illustrates the distinction with its “Hack failure” category: “The model makes the goal trivially provable by altering the formal meaning of the statement (e.g. redefining/shadowing key notions) rather than proving the intended theorem.” (Section 4.3, PDF p. 9).
Problem 59 succeeds after replacing an empty-codomain attempt with a constant functor from Type to a terminal category, then repairing universe and type errors. Problem 63 fails because the model neither supplies the needed connection between categorical finite presentability and the custom group-presentation predicate nor constructs the required filtered diagram; constant diagrams and tactic placeholders fail to supply that mathematics (Appendix E, PDF pp. 19–22).
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; resolve the paper’s statement-weight discrepancy before reproducing its scores
- 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 within a fixed budget
Last edited: