Towards Large Language Models as Copilots for Theorem Proving in Lean

arXiv:2404.12534v1 Announce Type: cross
Abstract: Theorem proving is an important challenge for large language models (LLMs), as formal proofs can be checked rigorously by proof assistants such as Lean, leaving no room for hallucination. Existing LLM-based provers try to prove theorems in a fully autonomous mode without human intervention. In this mode, they struggle with novel and challenging theorems, for which human insights may be critical. In this paper, we explore LLMs as copilots that assist humans in proving theorems. …

abstract arxiv assistants autonomous challenge copilots cs.ai cs.lg cs.lo fully autonomous hallucination human human intervention language language models large language large language models lean llm llms prove room stat.ml theorem type