Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
RocqPL 2027 Call for Presentations
Wed 2026/09/09
JFLA 2027: Second Appel à Communications
Tue 2026/09/08
Chaire de Professeur Junior in Lyon: Generative AI for formal proofs
Thu 2026/08/27
ANU International Logic Summer School, 7–18 December
Sun 2026/08/23
Call for Nominations: POPL 2027 Artificat Evaluation Committee
Tue 2026/08/18
Mathcomp 2.6.0 released
Tue 2026/08/18
We are paying math researchers to capture the work you are already doing!
Mon 2026/08/17
Tree-sitter grammar for Rocq (release 0.2.0)
Mon 2026/08/10
MITACS Undergrad Research Internships - 2027 Applications Open
Fri 2026/08/07
Rocq Platform release 2026.07.0 with Rocq 9.1
Thu 2026/08/06
Zulip
AI agents for writing proofs
Ocaml recommended version
Pattern matching on primitive int
Complexity Theory
The first baby steps with arrays in VST
How can Rocq termination checker handle List.map?
pattern tactic on a subterm
✔ Flocq: nearest float to a real
Indentation with Emacs
Essential mailing lists for Rocq users
Proof Assistants Stack Exchange
Make [...] explicit in Rocq/vsRocq
1 answer
Wed 2026/09/02
Non-typed dependent pattern matching in Rocq
1 answer
Thu 2026/08/20
An upgrade from Mathcomp v2.4.0 to v2.5.0 going wrong with rationals
1 answer
Sat 2026/08/15
Error when making CoqProject
2 answers
Mon 2026/08/03
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Sun 2026/08/02
Induction COQ Question
2 answers
Sun 2026/08/02
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Fri 2026/07/31
Declaring builders with Hierarchy Builder (Rocq)
1 answer
Thu 2026/07/16
Formalizing "finite or infinite" in Coq/Rocq
5 answers
Thu 2026/07/16
What is the best way to learn Iris completely independently
3 answers
Thu 2026/07/16
CS Theory Stack Exchange
Is injectivity of constructors for (large) inductive types in Prop, such as squashing, consistent?
Mon 2026/04/27
Finite sets in Coq
1 answer
Fri 2025/01/31
Representations of Planar Graphs in Coq
2 answers
Wed 2025/01/08
Simple Coq simplification question
1 answer
Fri 2024/06/07
What should a proof of correctness for a typechecker actually be proving?
3 answers
Thu 2024/06/06
Formalization of matching logic (logic behind K Framework)
3 answers
Wed 2023/08/16
Notation problem
1 answer
Thu 2023/06/01
Can I define nested mutually dependent types in Coq?
1 answer
Sat 2023/05/13
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2023/04/25
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
3 answers
Thu 2023/03/23
Stack Overflow
Trouble with well-foundedness proofs
Sat 2026/07/11
How to get the fully qualified name of a Rocq tactic?
2 answers
Wed 2026/06/24
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
1 answer
Wed 2026/05/20
Which vector library to use in coq?
2 answers
Sun 2026/03/22
Can we prove equal subcases have equal induction hypotheses in recursion principle?
5 answers
Tue 2026/02/24
Coq (Rocq) standard library function for converting nat to string?
1 answer
Wed 2026/02/11
Equality of type with equal indices do not typecheck
3 answers
Wed 2026/01/28
How to prove manually (using calc) a Dafny lemma with an existential variable?
3 answers
Sun 2026/01/25
Kind of issue with two-steps recursion
2 answers
Fri 2026/01/09
How to scrutinize a `match` term with return type `a=b -> c`
1 answer
Mon 2025/10/20
