3 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
Turing machines deciders, part I
The bbchallenge Collaboration, Justin Blanchard, Konrad Deka +9
The Busy Beaver Challenge (or bbchallenge) aims at collaboratively solving the following conjecture: "" [Radó, 1962], [Marxen and Buntrock, 1990], [Aaronson…
cs.LO2024
Hardness of busy beaver value BB(15)
Tristan Stérin, Damien Woods
The busy beaver value BB(n) is the maximum number of steps made by any n-state, 2-symbol deterministic halting Turing machine starting on blank tape. The busy beaver function $n \m…