Library Before Proof: Making LLM-Generated Rocq Usable by Mathematicians
A three-artifact approach is proposed: 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.
Guillaume Baudart, Marc Lelarge
· 0 citations