LemmaHead: RAG Assisted Proof Generation Using Large Language Models

Tianbo Yang, Mingqi Yan, Hongyi Zhao +1

Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the…