Leandojo Lean4 Tacgen Byt5 Small

🚀 LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

LeanDojo is a project for theorem proving using retrieval-augmented language models. It offers a new approach to theorem proving and is presented at NeurIPS (Datasets and Benchmarks Track) in 2023.

🚀 Quick Start

For detailed information, please visit LeanDojo Website.

📄 License

This project is licensed under the MIT license.

📚 Documentation

Inference Parameters

Widget Example

The widget has an example with the text "a b : ℕ\n⊢ a + b = b + a" and the example title "Example".

Paper Information

• Title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
• Conference: NeurIPS (Datasets and Benchmarks Track), 2023
• Authors: Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar

BibTeX Citation

@inproceedings{yang2023leandojo,
    title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
    author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
    booktitle={Neural Information Processing Systems (NeurIPS)},
    year={2023}
}