This page aggregates several resources related to automating proofs (and programs) in the Lean programming language.

Tactics

• LeanHammer (training repo) – A tactic that performs machine-learning premise selection, translation to SMT and proof reconstruction back to Lean.
• Aesop is a tactic that performs white-box proof search. You annotate lemmas with tags so they can be used in Aesop, both in forward or backwards style. It can be seen as a much more powerful simp tactic.
• LLMStep a tactic that uses LLMs to suggest the next tactic
• Lean GPTf A tactic that uses ChatGPT to suggest tactics

Writing Tactics and Metaprogramming in Lean

• Lean4 Metaprogramming Book
• Metaprogramming in Lean by Evgenia Karunus

Extracting theorems from Lean and MathLib

Mostly from Python scripts.

• Lean Step processing scripts lean step is a tactic that predicts the next tactic using LLMs
• Lean TPE Theorem Proving environment
• Lean Gym Gym-style API
• Lean LSP MCP MCP server that uses the LSP of Lean
• lean client Python API to interact with the Lean4 language server
• Lean Tool a Python (and MCP) tool to interact directly with lean
• Leanabell Reinforcement Learning Theorem Proving