LeanIDE: Next-Generation Integrated Development Environment for Formal Mathematics

Will Adkisson1, Ryan Hsiang2, Robert Joseph George2, Anima Anandkumar2
1Washington University
2California Institute of Technology
GitHub

Vision and Mission

LeanIDE represents the culmination of our research program in neuro-symbolic AI for formal mathematics. Building upon the foundational infrastructure of LeanDojo, the intelligent assistance of LeanCopilot, the lifelong learning capabilities of LeanAgent, and the search optimization of LeanProgress, LeanIDE aims to create the ultimate development environment for formal mathematics.


This integrated platform addresses the grand challenge of making formal mathematics accessible to a broader community by providing an intuitive, AI-powered environment that seamlessly combines human mathematical intuition with machine computational power.

LeanIDE Demo


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

Integrated AI-Powered Features

LeanIDE will integrate all components of our research ecosystem into a unified development experience:


LeanDojo Integration

Direct access to the comprehensive LeanDojo infrastructure for data extraction, proof interaction, and mathematical library exploration.

LeanCopilot Assistant

Built-in intelligent copilot providing real-time tactic suggestions, premise selection, and interactive proof guidance.

LeanAgent Learning

Lifelong learning capabilities that continuously improve based on user interactions and proof development patterns.

LeanProgress Optimization

Advanced search guidance using proof progress prediction to optimize theorem proving efficiency and success rates.

Intelligent Visualization

Advanced proof tree visualization, mathematical concept mapping, and interactive exploration of formal mathematical structures.

Collaborative Platform

Real-time collaboration features enabling distributed teams to work together on complex mathematical formalization projects.

Development Status

LeanIDE is currently in the conceptual design phase as we continue developing the foundational technologies. Follow our research progress and contribute to the vision on GitHub.