Formalizing Natural Language Proofs in Lean using Large Language Models
Proof assistants like Lean require substantial human effort to guide proof construction. However, recent advances in machine learning, particularly with Large Language Models (LLMs), suggest new possibilities for automation. This project will explore how LLMs can iteratively refine natural language proofs into formal proofs, reducing the manual effort required for formalization. Using the Delphyne framework – which introduces a new foundational paradigm for building modular and reliable LLM-enabled software – you will develop a pipeline for formalizing mathematical arguments in Lean, using a creative combination of prompting, search and domain-specific knowledge.
Prior experience with Lean would be appreciated. For more information, please reach out to jonathan.laurent@kit.edu.