# CoqPilot, a plugin for LLM-based generation of proofs

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 20 references that are in the map.
- First posted on arXiv 25 Oct 2024.

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

- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [QED at Large: A Survey of Engineering of Formally Verified Software](https://mlsanity.com/paper/2003.06458/) (2020)

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

- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Locus: Agentic Predicate Synthesis for Directed Fuzzing](https://mlsanity.com/paper/2508.21302/) (2025)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity](https://mlsanity.com/paper/2502.11901/) (2025)
- [ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving](https://mlsanity.com/paper/2502.04671/) (2025)
- [RocqSmith: Can Automatic Optimization Forge Better Proof Agents?](https://mlsanity.com/paper/2602.05762/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)
- [Position: Intelligent Coding Systems Should Write Programs with Justifications](https://mlsanity.com/paper/2508.06017/) (2025)
- [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026)

## Abstract (arXiv)

We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e., proof holes, and combines LLMs along with non-machine-learning methods to generate proof candidates for the holes. Then, CoqPilot checks if each proof candidate solves the given subgoal and, if successful, replaces the hole with it. The focus of CoqPilot is twofold. Firstly, we want to allow users to seamlessly combine multiple Coq generation approaches and provide a zero-setup experience for our tool. Secondly, we want to deliver a platform for LLM-based experiments on Coq proof generation. We developed a benchmarking system for Coq generation methods, available in the plugin, and conducted an experiment using it, showcasing the framework's possibilities. Demo of CoqPilot is available at: https://youtu.be/oB1Lx-So9Lo. Code at: https://github.com/JetBrains-Research/coqpilot