CoqPilot, a plugin for LLM-based generation of proofs. - Andrei Kozyrev; Gleb Solovev; Nikita Khramov; Anton Podkopaev (ASE, 2024)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation. - Nikita Khramov; Andrei Kozyrev; Gleb Solovev; Anton Podkopaev (CoRR, 2025)