arXiv:2611.09048 · v1

LeanDojo-v2: A Comprehensive Library for AI-Assisted Theorem Proving in Lean

首次提交 2026-11-06 14:21

版本更新 2026-11-06 14:21

雷达观测 2026-11-09 11:19

摘要

Building on recent progress in machine learning for formal theorem proving in Lean, we introduce LeanDojo-v2: an end-to-end framework that unifies repository data extraction, LLM fine-tuning, proof search, AI autocompletion, and LLM-assisted theorem proving in a single software library. In addition, we provide Lean4Code, a lightweight IDE that integrates the various features of LeanDojo-v2 through a simple, mathematician-friendly UI. These tools will enable mathematicians and researchers to easily fine-tune language models on domain-specific Lean codebases and experiment with LLM-assisted theorem proving without a complex setup.

作者备注：11 pages, 7 figures, accepted to NeurIPS Math-AI workshop