#rocq

Guillaume Laforge

@glaforge.dev

3 weeks ago

Comparing #Lean and #Rocq (Coq)
I thought both were theorem provers, but it seems Rocq is more for building verifiable software, while Lean is for more classical math.
So Lean might be a better fit for the math explorations #LLMs and #AI #Agents are doing for solving problems.

José A. Alonso

@jalonso.eurosky.social

2 months ago

Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. dl.acm.org/doi/pdf/10.1... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

Readings shared December 29, 2025 The readings shared in Bluesky on 29 December 2025 are: Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT The biggest controversy in maths coul

Readings shared December 29, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT

José A. Alonso

@jalonso.eurosky.social

2 months ago

Tacq: Context aware tactic recommendation for Rocq. ~ Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias, Marc Lelarge, Theo Stoskopf. hal.science/hal-05428166... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

Formalisation de la stabilité de l’erreur d’estimation de l’inclinaison d’un robot. ~ Lynda Bentoucha, Reynald Affeldt. hal.science/hal-05428166... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

Une sémantique de Kahn mécanisée pour les machines à états. ~ Timothy Bourke, Paul Jeanmaire, Marc Pouzet. hal.science/hal-05428166... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

Formal verification of Borrow-Checking by local commutation diagrams. ~ Alban Reynaud Michez. hal.science/hal-05428143/ #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

The machine-checked complete formalization of Landau’s foundations of analysis in Rocq. ~ Yue Guan, Yaoshun Fu, Xiangtao Meng. www.mdpi.com/2227-7390/14... #ITP #Rocq #Math

José A. Alonso

@jalonso.eurosky.social

2 months ago

Readings shared December 19, 2025 The readings shared in Bluesky on 19 December 2025 are: Proof engineering for program logics in Isabelle/HOL. ~ Chelsea L. Edmonds. #ITP #IsabelleHOL Modular proofs in Isabelle/HOL. ~ Chelsea L. Edmo

Readings shared December 19, 2025. jaalonso.github.io/vestigium/po... #AI #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

José A. Alonso

@jalonso.eurosky.social

2 months ago

Prediction: AI will make formal verification go mainstream. ~ Martin Kleppmann. martin.kleppmann.com/2025/12/08/a... #AI #LLMs #ITP #LeanProver #IsabelleHOL #Rocq

terrorist :: Feline

@majoranaoedipus.mathstodon.xyz.ap.brid.gy

3 months ago

50 years of proof assistants
lawrencecpaulson.github.io//2025/12/05/History_of_P...

#ProofAssistant #Isabelle #Coq #Rocq #LCF #HOL

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 14, 2025 The readings shared in Bluesky on 14 December 2025 are: A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. #ITP #Rocq A modular Lean 4 framework for confluence and strong normalization of lambda

Readings shared December 14, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq

José A. Alonso

@jalonso.eurosky.social

3 months ago

A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. joomy.korkutblech.com/papers/game-... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 5, 2025 The readings shared in Bluesky on 5 December 2025 are: Formalization of Erdős problems. ~ Boris Alexeev. #ITP #LeanProver #Math #Autoformalization A Rocq formalization of monomial and graded orders.

Readings shared December 5, 2025. jaalonso.github.io/vestigium/po... #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3

José A. Alonso

@jalonso.eurosky.social

3 months ago

A Rocq Formalization of Monomial and Graded Orders Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method....

A Rocq formalization of monomial and graded orders. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. arxiv.org/abs/2512.04573 #ITP #Rocq #Math

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 2, 2025 The readings shared in Bluesky on 2 December 2025 are: The machine translation of Landau’s analysis of foundations in Rocq. ~ Yue Guan, Yaoshun Fu, XiangTao Meng. #ITP #Rocq #Math Formalization of br

Readings shared December 2, 2025. jaalonso.github.io/vestigium/po... #AI #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared November 25, 2025 The readings shared in Bluesky on 25 November 2025 are: Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L

Readings shared November 25, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Programming #Rocq

José A. Alonso

@jalonso.eurosky.social

3 months ago

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language ...

MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. arxiv.org/abs/2503.04763 #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared November 23, 2025 The readings shared in Bluesky on 23 November 2025 are: DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof Verified certification

Readings shared November 23, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq

José A. Alonso

@jalonso.eurosky.social

3 months ago

Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. www.insmi.cnrs.fr/fr/cnrsinfo/... #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 14, 2025 The readings shared in Bluesky on 14 November 2025 are: An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math Choice trees: Representing and

Readings shared November 14, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #Rocq

José A. Alonso

@jalonso.eurosky.social

4 months ago

Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. ~ Nicolas Chappe et als. www.cambridge.org/core/journal... #ITP #Rocq

José A. Alonso

@jalonso.eurosky.social

4 months ago

Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. hal.science/hal-05342510... #ITP #LeanProver #Rocq

Tim Makarios

@tmakarios.theres.life.ap.brid.gy

4 months ago

I've been thinking about something that's related to Tarski's undefinability theorem (and might possibly be a corollary if viewed from the right angle), but relates to computability rather than truth. It seems to have implications for systems like Agda and Rocq, which I don't have much […]

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared October 29, 2025 The readings shared in Bluesky on 29 October 2025 are: Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #ITP #LeanProver #Math 1000+ theorems (The spiritual successor of Free

Readings shared October 29, 2025. jaalonso.github.io/vestigium/po... #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq

José A. Alonso

@jalonso.eurosky.social

4 months ago

1000+ theorems (The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!). ~ Katja Berčič et als. 1000-plus.github.io/all #Math #ITP #IsabelleHOL #HOL_Light #Rocq #LeanProver #Metamath #Mizar

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared October 21, 2025 The readings shared in Bluesky on 21 October 2025 are: HITrees: Higher-order interaction trees. ~ Amir Mohammad Fadaei Ayyam, Michael Sammler. #ITP #LeanProver Certifying optimal MEV strategies with

Readings shared October 21, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

José A. Alonso

@jalonso.eurosky.social

4 months ago

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Interactive Theorem Proving was repeatedly shown to be fruitful combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation and illuminates potential a...

RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Andrei Kozyrev, Nikita Khramov, Gleb Solovev, Anton Podkopaev. arxiv.org/abs/2505.22846 #ITP #Rocq #LLMs

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared October 18, 2025 The readings shared in Bluesky on 18 October 2025 are: An introduction to formal real analysis (Lecture 12: Cauchy sequences II). ~ Alex Kontorovich. #ITP #LeanProver #Math Pushdown automata (in Isab

Readings shared October 18, 2025. jaalonso.github.io/vestigium/po... #AI #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

José A. Alonso

@jalonso.eurosky.social

4 months ago

Functional Reasoning for Distributed Systems with Failures Distributed system theory literature often argues for correctness using an informal, Hoare-like style of reasoning. While these arguments are intuitive, they have not all been foolproof, and whether t...

Functional reasoning for distributed systems with failures. ~ Haobin Ni, Robbert van Renesse, Greg Morrisett. arxiv.org/abs/2510.121... #ITP #Rocq