mlsanityData to 14 Oct 2026

The Lean mathematical library

arXiv 1910.09336 ↗First posted 21 Oct 2019cs.LO math.LOcited by 134

Not on the map. Why?

Cited by 23 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led us here.

Key facts. Cited by 134 papers in the map (data through 14 Oct 2026). First posted on arXiv 21 Oct 2019.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 3; 2022: 2; 2023: 13; 2024: 19; 2025: 28; 2026: 69.

134 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2023Llemma: An Open Language Model For Mathematicscited by 388
  4. 2023Mathematical Capabilities of ChatGPTcited by 268
  5. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  6. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  7. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  8. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  9. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  10. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  11. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  12. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 119
38 more
  1. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  2. 2023Scaling Transformer to 1M tokens and beyond with RMTcited by 98
  3. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
  4. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  5. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  6. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
  7. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  8. 2023Scalable AI Safety via Doubly-Efficient Debatecited by 57
  9. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  10. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  11. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 37
  12. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  13. 2025VERINA: Benchmarking Verifiable Code Generationcited by 34
  14. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  15. 2024Reliable Evaluation and Benchmarks for Statement Autoformalizationcited by 32
  16. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 31
  17. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
  18. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 29
  19. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  20. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  21. 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
  22. 2024Machine learning and information theory concepts towards an AI Mathematiciancited by 20
  23. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  24. 2024miniCodeProps: a Minimal Benchmark for Proving Code Propertiescited by 18
  25. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 18
  26. 2026A Minimal Agent for Automated Theorem Provingcited by 18
  27. 2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 17
  28. 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 15
  29. 2024Reliable Reasoning Beyond Natural Languagecited by 14
  30. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 12
  31. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 11
  32. 2023Machine-Learned Premise Selection for Leancited by 10
  33. 2023A New Approach Towards Autoformalizationcited by 10
  34. 2024ImProver: Agent-Based Automated Proof Optimizationcited by 10
  35. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 10
  36. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 10
  37. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 10
  38. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8

50 most cited of 134 All 134 (JSON)