A curated collection of resources for learning Lean 4 and applying it to AI research
The standard textbook for learning theorem proving in Lean 4. Start here.
BookLearn Lean 4 as a general-purpose functional programming language.
BookAn interactive tutorial on formalizing mathematics in Lean 4 with Mathlib.
TutorialA fun, interactive browser game that teaches Lean 4 proof tactics through natural number proofs.
InteractiveAn open-source playground for LLM-based theorem proving in Lean. Provides tooling, data extraction, and interaction with Lean.
FrameworkAn LLM-based tactic suggestion tool that integrates directly into Lean 4's VS Code extension.
ToolTools for programmatically interacting with Lean 4 from Python for reinforcement learning setups.
FrameworkA large-scale dataset of Lean 4 problems for training and evaluating AI provers.
DatasetBenchmark datasets extracted from Mathlib for evaluating theorem provers.
BenchmarkThe Lean 4 math library itself -- a massive corpus of formalized mathematics with 100k+ theorems.
CorpusA cross-system benchmark of formalized math olympiad problems, available in Lean 4.
BenchmarkNatural language search for Lean theorems and lemmas. Describe what you need in English.
SearchThe primary community hub. Active discussions on Lean, Mathlib, tactics, and AI.
ChatCommunity-maintained guides, tutorials, installation instructions, and contribution info.
CommunityThe official Lean 4 repository. Report issues, track development, and contribute.
SourceThe community math library. One of the largest formalized math projects in the world.
SourceYang et al., 2023. Introduces LeanDojo and ReProver for LLM-based proving.
NeurIPS 2023Jiang et al., 2023. Combines informal and formal reasoning for theorem proving.
ICLR 2023Polu & Sutskever, 2020. The GPT-f paper that started the LLM+theorem proving wave.
FoundationalXin et al., 2024. Advancing LLM-based theorem proving with proof search and RL.
2024