We build open-source tools that connect large language models to the Rocq (formerly Coq) proof assistant — from interactive proof development to large-scale ML training pipelines.
| Project | Description |
|---|---|
| Pytanque | Python API for lightweight communication with Rocq via coq-lsp — backbone of the other tools |
| Rocq-MCP | MCP server that gives AI agents direct access to the Rocq prover: compile, step through proofs, query the environment, and verify results |
| Rocq Skills | Host-agnostic workflow pack (Claude Code, Codex, Gemini CLI, Cursor, …) with prove / review / golf loops, library search, and safety guardrails |
| rocq-ml-toolbox | Scalable inference server, proof/AST parser, Docker helpers, and safe proof-checking for ML training pipelines |
| Project | Description |
|---|---|
| miniF2F-rocq | Rocq translation of the miniF2F benchmark (from Lean/Isabelle) — arXiv:2503.04763 |
| Putnam2025-Rocq | 2025 Putnam Competition — 10/12 problems formalized and proved — arXiv:2603.20405 |
| Project | Description |
|---|---|
| CRRRocq | Chain-of-thought + RAG + recursive tool calling for Rocq proofs |
| Babel-Formal | Cross-prover proof translation between Rocq and Lean |
| LLM4Docq | Automatic docstring generation for MathComp |
| NLIR | Natural-language intermediate representations for Rocq proving (NeurIPS 2024 MATH-AI) |
- NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving Teodorescu, Baudart, Gallego Arias, Lelarge. NeurIPS 2024 Workshop MATH-AI. HAL
- MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study Viennot, Baudart, Gallego Arias, Lelarge. NeurIPS 2025 Workshop MATH-AI. arXiv:2503.04763
- Babel-Formal: Translation of Proofs between Lean and Rocq Stoskopf, Cohen, Tabareau. NeurIPS 2025 Workshop MATH-AI. HAL
- Tacq: Context Aware Tactic Recommendation for Rocq Viennot, Baudart, Gallego Arias, Lelarge, Stoskopf. JFLA 2026. HAL
- LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback Stoskopf, Viennot, Cohen. Rocqshop@ITP 2025. Abstract
- Putnam 2025 — Rocq Formalization arXiv:2603.20405
