Readings shared April 4, 2026 The readings shared in Bluesky on 4 April 2026 are: Why Lean?. ~ Leonardo de Moura. #LeanProver #ITP A formalization of the Gelfond-Schneider theorem. ~ Michail Karatarakis, Freek Wiedijk. #LeanProve

Readings shared April 4, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #Agda #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Programming #Prolog #Racket #RocqProver

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 Putna...

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

Readings shared March 9, 2026 The readings shared in Bluesky on 9 March 2026 are: Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP Formalization in Lean of faithfully flat descent of project

Readings shared March 09, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #LeanProver #Lisp #Math #Physics #RocqProver

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural ...

Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. arxiv.org/abs/2603.04006 #RocqProver #ITP

Readings shared March 4, 2026 The readings shared in Bluesky on 4 March 2026 are: When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP Formalising sphere packing in Lean. ~ Chris Birkbec

Readings shared March 04, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver

Mechanizing the proof of a borrow calculus. ~ Alban Reynaud Michez. hal.science/hal-05527340... #RocqProver #ITP

Readings shared March 1, 2026 The readings shared in Bluesky on 1 March 2026 are: Lean for science formalization. ~ Przemyslaw Chojecki. #LeanProver #ITP Vibe-coding a debugger for a DSL. ~ Joachim Breitner. #LeanProver Bidirecti

Readings shared March 01, 2026. jaalonso.github.io/vestigium/po... #ITP #LeanProver #RocqProver

Bidirectional interpolation for the lambda-calculus – Revisiting and formalising Craig-Čubrić interpolation. ~ Meven Lennon-Bertrand, Alexis Saurin. hal.science/hal-05526634... #RocqProver #ITP

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof wri...

Machine-generated, machine-checked proofs for a verified compiler (Experience report). ~ Zoe Paraskevopoulou. arxiv.org/abs/2602.20082 #RocqProver #ITP

Readings shared February 19, 2026 The readings shared in Bluesky on 19 February 2026 are: Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. #LeanProver #ITP

Readings shared February 19, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

A Rocq-based formalization of Hilbert’s geometry: Building a reusable foundation for 3D perpendicularity theory and verification. ~ Qimeng Zhang, Wensheng Yu. www.mdpi.com/2297-8747/31... #RocqProver #ITP #Math

Formal P‑category theory and normalisation for simple type theory. ~ David George Berry. www.repository.cam.ac.uk/bitstreams/e... #ITP #RocqProver

Readings shared January 24, 2026 The readings shared in Bluesky on 24 January 2026 are: Abel's limit theorem (in Isabelle/HOL). ~ Kangfeng Ye. #ITP #IsabelleHOL #Math A formalization of the downward Löwenheim-Skolem theorem in Coq.

Readings shared January 24, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver

The HOL-Light library of multivariate real analysis in Rocq. ~ Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. inria.hal.science/hal-05464922... #ITP #RocqProver #HOL-Light #Math

Formally verified number-theoretic transform. ~ Alix Trieu. cic.iacr.org/p/2/4/1 #ITP #RocqProver

Readings shared January 19, 2026 The readings shared in Bluesky on 19 January 2026 are: Broken proofs and broken provers. ~ Lawrence Paulson. #ITP #IsabelleHOL #RocqProver #LeanProver A formalization of Borel determinacy in Lean. ~

Readings shared January 19, 2026. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver

Broken proofs and broken provers. ~ Lawrence Paulson. lawrencecpaulson.github.io/2026/01/15/B... #ITP #IsabelleHOL #RocqProver #LeanProver

Readings shared January 14, 2026 The readings shared in Bluesky on 14 January 2026 are: A lambda-superposition tactic for Isabelle/HOL. ~ Massin Guerdi. #ITP #IsabelleHOL Adding sorts to an Isabelle formalization of superposition. ~

Readings shared January 14, 2026. jaalonso.github.io/vestigium/po... #AI #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver

Formal verification for JavaScript regular expressions: A proven mechanized semantics and its applications. ~ Aurèle Barrière, Victor Deng, Clément Pit-Claudel. dl.acm.org/doi/pdf/10.1... #ITP #RocqProver

Computation-tree semantics: An algorithmic approach to structurally defined relations. ~ Sean Kristian Remond Harbo, Hans Hüttel. dl.acm.org/doi/pdf/10.1... #ITP #RocqProver

Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies- dl.acm.org/doi/pdf/10.1... #ITP #RocqProver

Readings shared May 23, 2025 The readings shared in Bluesky on 23 May 2025 are A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math Solving guarded domain equations in

Readings shared May 23, 2025. jaalonso.github.io/vestigium/po... #AIforCode #CategoryTheory #ITP #IsabelleHOL #LLMs #LeanProver #Math #RocqProver

Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. tildeweb.au.dk/au571806/pub... #ITP #RocqProver #CategoryTheory