CoqPilot：基于大型语言模型的证明生成插件

本研究解决了Coq证明自动化书写的困难，提出了CoqPilot这个VS Code扩展。该插件结合了大型语言模型和非机器学习方法，自动生成满足证明需求的候选解，并提供了一个无须设置的用户体验和一个用于Coq证明生成实验的平台，具有重要的研究意义。