4 papers
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
Jules Viennot, Guillaume Baudart, Marc Lelarge
Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with pr…
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…
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:…
Automatic Rao-Blackwellization for Sequential Monte Carlo with Belief Propagation
Waïss Azizian, Guillaume Baudart, Marc Lelarge
Exact Bayesian inference on state-space models~(SSM) is in general untractable, and unfortunately, basic Sequential Monte Carlo~(SMC) methods do not yield correct approximations fo…