LeanDojo
The foundational infrastructure that bridges Python-based ML and the Lean prover, enabling data extraction and interactive environments for AI research. This work provides the essential tooling that makes all subsequent research possible.
LeanAgent
A lifelong learning framework for autonomous theorem proving that continuously improves across expanding mathematical domains without catastrophic forgetting. This represents our exploration of fully autonomous mathematical reasoning.
LeanCopilot
A human-in-the-loop assistant that seamlessly integrates LLMs into the Lean environment, providing real-time suggestions and proof automation. This work demonstrates effective human-AI collaboration in formal mathematics.
LeanProgress
A specialized s…
LeanDojo
The foundational infrastructure that bridges Python-based ML and the Lean prover, enabling data extraction and interactive environments for AI research. This work provides the essential tooling that makes all subsequent research possible.
LeanAgent
A lifelong learning framework for autonomous theorem proving that continuously improves across expanding mathematical domains without catastrophic forgetting. This represents our exploration of fully autonomous mathematical reasoning.
LeanCopilot
A human-in-the-loop assistant that seamlessly integrates LLMs into the Lean environment, providing real-time suggestions and proof automation. This work demonstrates effective human-AI collaboration in formal mathematics.
LeanProgress
A specialized system that provides global progress estimation for proof search, improving the efficiency of automated theorem proving through intelligent search guidance.
LeanIDE
An integrated development environment specifically designed for Lean theorem proving, combining modern IDE features with AI-powered assistance to create the ultimate platform for formal mathematics.