Proof Automation with Large Language Models

Minghai Lu, Benjamin Delaware, Tianyi Zhang

Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expe…