LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
CMSA Room G10 CMSA, 20 Garden Street, Cambridge, MA, United Stateshttps://youtu.be/u-pkmdkQoMU New Technologies in Mathematics Seminar Speaker: Alex Gu, MIT Dept. of EE&CS Title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Abstract: Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute […]