rocq-piler

scidonia/rocq-piler
★ 5 stars TeX 🤖 AI/LLM Updated today
MCP server for Coq LSP
View on GitHub → Try with Claude — $10 free →

Quick Install

Copy the config for your editor. Some servers may need additional setup — check the README.

Add to claude_desktop_config.json:

{
  "mcpServers": {
    "rocq-piler": {
      "command": "npx",
      "args": [
        "-y",
        "scidonia/rocq-piler"
      ]
    }
  }
}

README Excerpt

**Let rocq-piler do the heavy lifting for your proofs.** This project demonstrates how a **Language Server Protocol (LSP)** interface to the **Rocq proof assistant** (formerly Coq) enables **neurosymbolic programming**: the seamless integration of neural networks (LLMs) with symbolic reasoning systems (proof assistants).

Tools (12)

check_filecheck_rangedeep_conjdelete_stepedit_filefocus_proofinsert_tacticopen_goalsproof_statereset_prooftry_stepundo_step