Credits and Acknowledgements

Contributors

If your code has been merged into the LeanDojo repo and you would like your name to appear on this page, please feel free to edit this page and open a PR.

Developers

• Kaiyu Yang: Postdoctoral Scholar at Caltech

• Peiyang Song: Undergrad at UC Santa Barbara

• Rahul Chalamala: Undergrad at Caltech

Advisors

• Anima Anandkumar: Bren Professor at Caltech, Senior Director of AI Research at NVIDIA

Related Tools

LeanDojo draws on numerous existing tools for interacting with and extracting data from proof assistants. The author benefited a lot from the lessons he learned when designing and implementing CoqGym. LeanDojo’s interaction implementation partially incorporates lean-gym’s code but fixes some critical issues and expanded its functionality. When prototyping the data extraction part of LeanDojo, the author found Jason Rute’s lean_proof_recording helpful. Its design was a hacky but extremely clever piece of art. Fortunately, we didn’t have to follow that design thanks to Lean’s AST exporting mechanism (lean --ast --tsast --tspp) implemented by Mario Carneiro, Gabriel Ebner, and Daniel Selsam. LeanDojo’s mechanism for exporting Lean 4 ASTs is inspired by the conversations with Mario Carneiro during Kaiyu Yang’s visit to Hoskinson Center for Formal Mathematics (directed by Jeremy Avigad) at CMU.

Below is a list of related tools we’re aware of. Please reach out if we missed your work!

Lean 3

• lean_proof_recording

• lean-gym

• lean-client-python

Lean 4

• LeanInk

• lean-gym for Lean 4

• Daniel Selsam’s Lean 4 fork

• repl

Coq

• CoqGym

• GamePad

Isabelle

• PISA

HOL Light

• HOList

Others

• INT