Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.

翻译：证明助手使用户能够开发有关软件属性的机器校验证明。然而，这些证明助手的交互特性将大部分证明负担施加给用户，使得形式化验证成为一项复杂且耗时的任务。基于神经方法的近期自动化技术尝试解决此问题，但需要良好的编程支持来收集数据并与证明助手交互。本文提出CoqPyt——一个用于与Coq证明助手交互的Python工具。CoqPyt通过提供新颖特性（例如丰富前提数据的提取）改进了其他Coq相关工具。我们预期本工作将促进专为证明合成与修复设计的工具和技术（尤其是基于大语言模型的技术）的开发。介绍并演示CoqPyt的视频详见：https://youtu.be/fk74o0rePM8。