While Proof Assistants have been proven to be extremely helpful, they are also known for being extremely challenging to use, learn, and adapt to the large and diverse set of applicable use cases.

In the first part of this talk, we will present Flèche, a new document manager for the Rocq proof assistant that was originally designed for teaching Rocq. Flèche aims to make it easier to build enhanced proof assistants. It has been built taking into account extensive user and developer feedback, and provides a unique set of features and extensibility.

Flèche's aims are twofold: we want to provide a usable, production ready platform for people willing to extend proof assistants at the document level; while at the same time developing such document managers in a rigorous, scientific way.

In the second part, we will present specialized tools for LLM-assisted proofs. First, the petanque and rocq-mcp protocols, built on top of Flèche, enable the interaction between LLMs and the Rocq prover.

We can then design agents that leverage both natural language reasoning and interactive proof search to formalize mathematical proofs.

We also train specialized LLMs assistants to suggest tactics, search for relevant theorems, translate results from one proof assistant to another, or guide the interactions with these tools.