# Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code

arXiv: https://arxiv.org/abs/2403.12627 · HTML: https://mlsanity.com/paper/2403.12627/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 27 references that are in the map.
- First posted on arXiv 19 Mar 2024.

## Builds on (most cited first, 6 of 6)

- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search](https://mlsanity.com/paper/2402.08147/) (2024)
- [Deep Generation of Coq Lemma Names Using Elaborated Terms](https://mlsanity.com/paper/2004.07761/) (2020)
- [LLM Interactive Optimization of Open Source Python Libraries -- Case Studies and Generalization](https://mlsanity.com/paper/2312.14949/) (2023)
- [Learning to Format Coq Code Using Language Models](https://mlsanity.com/paper/2006.16743/) (2020)

## Built on by (most cited first, 1 of 1)

- [Clarifying Before Reasoning: A Coq Prover with Structural Context](https://mlsanity.com/paper/2507.02541/) (2025)

## Abstract (arXiv)

In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the specialized nature of Coq syntax and semantics poses unique challenges for Large Language Models (LLMs). Addressing this gap, we present a comprehensive dataset specifically designed to enhance LLMs' proficiency in interpreting and generating Coq code. This dataset, derived from a collection of over 10,000 Coq source files, encompasses a wide array of propositions, proofs, and definitions, enriched with metadata including source references and licensing information. Our primary aim is to facilitate the development of LLMs capable of generating syntactically correct and semantically meaningful Coq constructs, thereby advancing the frontier of automated theorem proving. Initial experiments with this dataset have showcased its significant potential; models trained on this data exhibited enhanced accuracy in Coq code generation. Notably, a particular experiment revealed that a fine-tuned LLM was capable of generating 141 valid proofs for a basic lemma, highlighting the dataset's utility in facilitating the discovery of diverse and valid proof strategies. This paper discusses the dataset's composition, the methodology behind its creation, and the implications of our findings for the future of machine learning in formal verification. The dataset is accessible for further research and exploration: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1