LeanDojo was the first opensource LLM+Lean framework. We continue to build and have new tools like Lean Copilot, Lean Agent, and Lean Progress that significantly enhance theorem proving workflows for mathematicians. All of our code is here : http://
github.com/lean-dojo/ Lean Dojo

→ View original post on X — @animaanandkumar