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.
LeanIDE is the first IDE for Lean. We hope people contribute and add more features to make it better for everyone.
Interactive demonstration of LeanIDE's integrated development environment for formal mathematics.
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.