Extraction and Search in Rocq: Theorems, Definitions and Their dependencies

Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven theorems to assist the current proof process. However, the current search command is limited to the environment of imported modules and cannot search for theorems outside of this scope. Furthermore, tool developers and researchers may want to obtain detailed information about theorems, such as theorem's names, statements, and dependencies. But there are currently no user-friendly and efficient tools available for extracting comprehensive information from Rocq projects. We introduce a Rocq theorem extraction and analysis tool, TheoremExtr, which is capable of analyzing theorem composition and extracting theorems, dependencies, and definitions from both parsing phase and runtime. We extracted 71,795 theorems and their dependencies from 32 open-source projects from the Rocq community. In addition, we extracted 27,481 definitions and their types among these projects. We also developed a website that supports cross-project similarity search for theorems and definitions. The tool is available at https://github.com/Rw1nd/TheoremExtr, and the search website is available at https://lemmasearch.com.

Readings shared May 25, 2026

The readings shared in Bluesky on 25 May 2026 are: Four–in-a-row in Rocq. ~ Laurent Théry. #RocqProver #ITP Advancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et al

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

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 from the 2025 Putnam Mathematical Competition. The MCP tools, designed with Claude by analyzing logs from a prior experiment on miniF2F-Rocq, encode a "compile-first, interactive-fallback" strategy. Running on an isolated VM with no internet access, the agent deployed 141 subagents over 17.7 hours of active compute (51.6h wall-clock), consuming approximately 1.9 billion tokens. All proofs are publicly available.

GitHub - MudroadWhite/Neo-Principia: Continuation on formalizing Principia Mathematica

Continuation on formalizing Principia Mathematica. Contribute to MudroadWhite/Neo-Principia development by creating an account on GitHub.

Readings shared May 19, 2026

The readings shared in Bluesky on 19 May 2026 are: A shallow dive into formal verification. ~ Vitalik Buterin. #LeanProver #ITP Decidable (Logic in Lean). #LeanProver #ITP #FunctionalProgramming Lean

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq

The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because it is the only available method-e.g., in certain modal logics-or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimizations. Moreover, we show how TableauxRocq can be used as a certifier for automated theorem provers by adapting the Goeland prover- that can already output Rocq terms-to output proofs in the TableauxRocq format. By using the power of reflection, thereby providing a fully certified proof checker for free, we show that Goeland's exported Rocq terms and TableauxRocq's proof certificates can be checked in a similar time frame without proof optimizations, and that the latter has strictly better performances in presence of Skolemization-related optimizations.

Rocq'n'Share 2026 registration | Framaforms.org

Readings shared May 9, 2026

The readings shared in Bluesky on 9 May 2026 are: A shallow embedding of Datalog in Lean. ~ Ramy Shahin. #LeanProver #ITP Bennett's conjecture in Lean 4: Counter-models for the PSR-reducibility of Sp

A General Formalised Framework for Reasoning About Display Calculi - Studia Logica

We encode Belnap’s basic theory of display calculi in the proof assistant Coq/Rocq version 8.18.0 and formalise the proof that Belnap’s conditions C2–C8 imply the cut-elimination theorem. Our framework allows us to formally prove meta-theoretic results such as Hilbert-completeness and derivability of explicit rules, such as cut, but also others if required. What makes our formalisation powerful is that it works entirely with an abstraction that can be instantiated to many possible logics and display calculi, although we make no attempt to precisely characterise the logics that can be properly displayed in our formalisation. For this reason, our work can be seen as a formalisation of a display calculus framework and a cut-elimination theorem for a wide range of display calculi. As examples, we apply our work to classical propositional logic (CPL), tense logic (Kt), and non-commutative non-associative Lambek calculus to obtain complete display calculi as well as formally proved cut-elimination theorems, but we believe our formalisation to be also applicable to many others. We also encoded a proof of the decidability of CPL that relies only on the structure of proofs within an additive display calculus for CPL. To our knowledge, our work is the first formalisation of a decidability result in display calculus. Moreover, all of our formal proofs are constructive as they never require the addition of the law of excluded middle in Coq’s environment (which is constructive by default), which means we were also able to extract computer programs from our proof of cut-elimination able to convert CPL/Kt/Lambek derivation trees into cut-free ones. As formal proofs are known to be significantly longer to write than usual pen-and-paper proofs, our work led to the development of a multitude of files of Coq code comprising more than 15,000 lines.