LeanDojo-v2

An end-to-end framework for training, evaluating and deploying AI theorem provers in Lean.

• Developer / Organization: LeanDojo team and contributors
• Category: Open-source skills & interfaces
• Purpose: Support training, evaluation and deployment of Lean theorem provers.
• Key features: End-to-end theorem-prover training, evaluation and deployment. The original LeanDojo repository directs new projects to v2.
• Availability: Open-source software; Apache-2.0
• License: Apache-2.0 (source (opens in a new tab))
• Website / Source code: https://github.com/lean-dojo/LeanDojo-v2 (opens in a new tab)
• Version: GitHub release v1.0.9
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01