3 ms·
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- hackandthink 3y ago"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."
- deleted 3y ago[deleted]