The readings shared in Bluesky on 15 April 2025 are

• Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. #ITP #IsabelleHOL
• First-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. #ITP #IsabelleHOL
• Proof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. #ITP #IsabelleHOL
• The Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. #ITP #IsabelleHOL #Math
• Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. ~ Numina & Kimi Team. #LLMs #LeanProver
• Mathematical reasoning & proofs. ~ Alistair Savage. #Math
• Decomposing factorial of 300K as the product of 300K factors larger than 100K. ~ Gustavo. #Programming #RacketLang #FunctionalProgramming #Math
• Emacs Lisp elements (A big picture view of the Emacs Lisp programming language). ~ Protesilaos Stavrou. #Emacs #Lisp
• The Barium experiment. ~ Tom Szilagyi. #CommonLisp
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". #LeanProver #IsabelleHOL #Math