# LeanIDE - IDE for Lean4

Will Adkisson1, Ryan Hsiang2, Robert Joseph George2, Anima Anandkumar2
1Washington University
2California Institute of Technology
Published as part of: LeanDojo-v2, NeurIPS Mathematical Reasoning and AI, 2025
Code

## About LeanIDE

LeanIDE is the first IDE for Lean. We hope people contribute and add more features to make it better for everyone.

## LeanIDE Demo

Your browser does not support the video tag.

Interactive demonstration of LeanIDE's integrated development environment for formal mathematics.

## Features

LeanIDE includes all the features in LeanDojo-v2: repository tracing, lifelong dataset management, retrieval-augmented agents, Hugging Face fine-tuning, external inference APIs, and progress prediction.