The Rocq Prover

Started 2026-10-24

Rocq is a proof assistant that I use on a daily basis these days. A proof assistant essentially consists of a programming language which is suitable for expressing theorems and proofs, and a checker that makes sure the proofs actually prove the corresponding lemmas. Other popular proof assistants include Lean and Isabelle.

Proof assistants are used by both mathematicians and computer scientists. Mathematicians use them to avoid loopholes in large and complex math proofs while computer scientists use them to ensure correctness in (often critical) software.

I got interested in Rocq probably in 2021 (thanks to the amazing results presented by the Csmith paper and Wikipedia surfing). However, I started hands-on learning only in 2023 when I enrolled for a PhD. Even under a great guidance, Rocq required real hard word just to get started. It is going to be the same for any other proof assistant. I want this section of my digital garden to be the most concise and useful Rocq entrypoint that I had once wished for.

Key Concepts

  • Workflow: First, you provide definitions (like what you mean by a prime number). Then you state your goals/lemmas/theorems. Proceed to write proofs. There are mechanisms like tactics to help you. Once written, ask the proof checker to verify the proofs actually prove the lemmas in question.
  • Theory: Theorems are types and proofs are programs. Proof checking is typechecking. See Curry-Howard correspondence.

Getting Rocq

  • To get started with Rocq, maybe try the Web IDE first. It will take a while to load. If you are too impatient to read the instructions, open the scratchpad, type Goal nat. exact 13. Qed. (including the last fullstop) in the main editor area, and then press the Alt+Down a couple of times. It will show "no more goals" because you have proven natural numbers exist by giving 13 as a witness.
  • Installed offline, one could use Rocq inside Emacs, VSCodium, or the RocqIDE. Visit the official website for (partial) installation instructions.

Learning Theorem Proving

Hot and Controversial

Rocq has been in use in both academia and (select) industry for a long time. However, theorem provers in general have gained significant boost in the recent LLM boom. The key attraction is, unlike in many other areas, you don't have to trust LLMs here since the generated proofs are always checked in the traditional way by trustworthy proof checkers. However, ethical and legal issues aside, this can still be problematic if the modeling and lemmas are also provided by the LLM. Following links are just to demonstrate how hot proof assistants are right now; I have zero knowledge in Navier-Stokes.