A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL

Qiyuan Xu, Renxi Wang, Peixin Wang +2

Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using na…