Hello all,
The first public release of `boulodrome` is finally available !
It is a MCP server for Rocq/Coq proof assistance via the Pétanque protocol
Boulodrome gives LLMs interactive access to the Rocq proof assistant.
It exposes tools for starting proof sessions, running tactics, inspecting goals, searching the library, and undoing steps, turning theorem proving into a tool-calling loop. Since it is using Rocq as a library from OCaml, the latency is very low.
For now it is only working with Rocq 9.1, on project managed by dune.
Let me know what you think about it !
5 Likes
The logic field seems pretty much divided between LLM-enthousiast people (like Mark Tarver) and LLM-sceptic people (like John F. Sowa).
I am glad a proof assistant can now benefit LLM guidance and LLMs can benefit Rocq/Coq certification. This could be a giant step in the debate, do LLMs only mimic or are they creative ?
Edit: i have searched ‘boulodrome #announcements’ at https://discourse.rocq-prover.org/ but found nothing 
Hello and thanks for your reply ! Thanks for the head’s up, I’ll post an announcement also there by tomorrow !
Philosophical concerns aside (but they are nevertheless very interesting), I think the combination of logic proofs and LLM very fruitful : the LLM can access a truth oracle that can never drift and rejects hallucinations, and on the other side the human do not have the burden of proof redaction anymore; thus more time can be allocated to finding what needs to be proven.
In the 1980s there was a proof-formalization system called Mizar from behind the Iron Curtain. Polish. They had a surplus of mathematicians, and they formalized an impressive body of mathematics. The only automation was resolution, so “small steps”. When these LLM assists for proof-systems started appearing, I thought to myself: “sure, it’s not perfect, but if you think of it as just a souped-up version of that resolution stuff, it makes sense”. And it seems like it doesn’t matter if all it does is “ape” humans’ proof-steps: if it can apply some pattern that a human came up with in some other proof, and that succeeds, hey, it’s a win!
And I also thought: “the process of translating human-readable math statements into Coq’s Gallina or some other proof-language must surely be something that LLMs would be good at – it isn’t terribly deep, and that’s not where the deep thought in a proof is anyway.”
And I’m not a big fan of AI generally, so this is coming from a real skeptic.
2 Likes