CoqPilot, a plugin for LLM-based generation of proofs

Andrei Kozyrev, Gleb Solovev, Nikita Khramov +1

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.,…