LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

"We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research."