2 papers
cs.LG2026
Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Guillaume Baudart, Marc Lelarge, Tristan Stérin +1
We report on an experiment in which Claude Opus~4.6, equipped with a suite of Model Context Protocol (MCP) tools for the Rocq proof assistant, autonomously proved 10 of 12 problems…
cs.LO2025
MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias +1
In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources:…