Library Before Proof: Making LLM-Generated Rocq Usable by Mathematicians

LLM-assisted formalization now produces thousands of lines of Lean or Rocq for research-level mathematics, but the resulting code remains hard to read for a working mathematician who is not a Rocq expert. We argue that the bottleneck is no longer closing goals, but the library built \emph{around} the proof terms. We propose a three-artifact approach: mathcomp-style Rocq backed by an explicit coding-style skill, a Lean-style blueprint cross-linking informal math to formal lemmas, and a verification PDF pairing each definition and theorem statement with its informal version. We demonstrate it on two case studies: a textbook chapter of Stanley's \emph{Enumerative Combinatorics} and a Rocq formalization of Quasi-Borel Spaces. Both libraries contain zero \texttt{Admitted} and zero custom axioms; both were produced in a single Docker environment by Claude~Opus driving Rocq through an MCP server, to which we contributed. The contribution is not the libraries themselves but a proposal for the artifacts that should accompany LLM-generated Rocq for the mathematicians, plus the tooling to produce them.