#rocqprover — Public Fediverse posts

Readings shared July 27, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/27-readings_shared_07-27-26 #AI #AI4Math #Agda #Aristotle #ITP #IsabelleHOL #LeanProver #Logic #Math #Prolog #RocqProver

Formalising standard deontic logic and dyadic deontic logic in Rocq. ~ Sophie Krijgsman. https://www.cs.ru.nl/bachelors-theses/2026/Sophie_Krijgsman___1072493___Formalising_Standard_Deontic_Logic_and_Dyadic_Deontic_Logic_in_Rocq.pdf #RocqProver #ITP #Logic

Readings shared July 20, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/20-readings_shared_07-20-26 #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #PVS #RocqProver

Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP

Readings shared July 13, 2026. https://jaalonso.github.io/vestigium/posts/2026/07/13-readings_shared_07-13-26 #AI4Math #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. https://arxiv.org/abs/2505.07681 #RocqProver #ITP #FunctionalProgramming

I understand that there are editorial conventions for this, and I would like my opinion on the matter to be known, to wit:
1. Those editorial conventions are wrong, and
2. If I read this in an article, I will assume that the writer pronounces it "a mhll language."

#RocqProver #FormerlyKnownAsCoq

Extraction and search in Rocq: Theorems, definitions and their dependencies. ~ Jian Fang, Yingfei Xiong. https://arxiv.org/abs/2606.04704v1 #RocqProver #ITP

Readings shared May 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/25-readings_shared_05-24-26 #AI4Math #ATP #ITP #LeanProver #Math #RocqProver

Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. https://arxiv.org/abs/2603.20405 #AI4Math #RocqProver

Four–in-a-row in Rocq. ~ Laurent Théry. https://inria.hal.science/hal-05625464/document #RocqProver #ITP

Readings shared May 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/20-readings_shared_05-19-26 #AI4Math #FunctionalProgramming #ITP #LeanProver #Math #RocqProver

TableauxRocq: A deep embedding of free-variable tableaux in Rocq. ~ Johann Rosain, Julie Cailler. https://arxiv.org/abs/2605.16952v1 #RocqProver #ITP

**Rocq’n’Share 2026**
**Jun 29–Jul 3, EPFL**
Registration free but required: https://framaforms.org/rocqnshare-2026-registration-1769966293
More details: https://proofs.swiss/rocq-n-share/2026/

Are you itching to learn more about the internals of your favorite proof assistant? Do you have a feature to advocate for? Do you need help implementing an extension or hacking the kernel? Do you feel ready to step up and fix that bug that's been pestering you for years?

Join us for Rocq’n’Share! (contd. in thread)

#rocq #rocqprover

Readings shared May 9, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/10-readings_shared_05-09-26 #AI4Math #ATP #Aristotle #CompSci #CoqProver #FunctionalProgramming #Haskell #History #ITP #IsabelleHOL #LeanProver #Logic #Math #Mizar #Ocaml #RocqProver

It’s neat to see that an old (fiddly, complicated) decidability argument I wrote up in the 1990s is getting some attention. Here, Raj Goré and Anthony Peigné formalise (and generalise) my decidability argument for display formulations of some substructural logics. This is interesting work, worth looking into.

https://link.springer.com/article/10.1007/s11225-026-10239-8

#logic #prooftheory #rocqprover

A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic

Readings shared April 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/25-readings_shared_04-24-26 #AI4Math #Autoformalization #CompSci #CoqProver #FunctionalProgramming #HOL #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Nqthm #RocqProver

A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect. ~ Jean-Philippe Chancelier. https://arxiv.org/abs/2604.21376 #RocqProver #ITP #Math

On reasoning-centric LLM-based automated theorem proving. ~ Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong. https://arxiv.org/abs/2604.19558v1 #RocqProver #AI4Math

A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. https://arxiv.org/abs/2604.20345v1 #RocqProver #ITP #Math

A constructive proof of Rice's theorem and the halting problem via Hilbert's tenth problem. ~ Jonathan Brossard. https://arxiv.org/abs/2604.16477v1 #RocqProver #ITP #Math

Readings shared April 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/15-readings_shared_04-14-26 #AI4Math #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver

CARVe in Rocq: A library for substructural meta-theory. ~ Daniel Zackon et als. https://momigliano.di.unimi.it/papers/itp26.pdf #RocqProver #ITP

Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire

Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. https://arxiv.org/abs/2603.20405v1 #RocqProver #AI4Math

Readings shared March 09, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/10-readings_shared_02-09-26 #AI #AI4Math #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #LeanProver #Lisp #Math #Physics #RocqProver