LeanIDE is the first IDE for Lean. We hope people contribute and add more features to make it better for everyone. It brings project navigation, source editing, and interactive proof development into one environment, with the goal of making Lean more approachable for formal mathematics, software verification, and scientific computing.
LeanIDE is developed as part of LeanDojo-v2 and is intended to grow through open collaboration. We welcome contributions to the editor, proof interaction, visualizations, integrations, documentation, and user experience, as well as ideas for features that would make Lean more useful to a broader community.