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 #CSLib #CompSci
• Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. #LeanProver #ITP #CSLib #CompSci
• Pursuit of truth and beauty in Lean 4: Formally verified theory of grammars, optimization, matroids. ~ Martin Dvorak. #LeanProver #ITP #Math #CompSci
• Translating proofs from Lean to Dedukti. ~ Rishikesh Vaishnav. #LeanProver #Dedukti #ITP
• From sets in math to types in Lean: Subtype, Fin, Set, Finset, and Fintype. ~ Rado Kirov. #LeanProver #ITP
• Towards real-world industrial-scale verification: LLM-driven theorem proving on seL4. ~ Jianyu Zhang et als. #IsabelleHOL #ITP #LLMs
• Towards term-based verification of diagrammatic equivalence. ~ Julie Cailler, Noé Delorme, Simon Perdrix, Sophie Tourret. #IsabelleHOL #ITP
• A Rocq-based formalization of Hilbert’s geometry: Building a reusable foundation for 3D perpendicularity theory and verification. ~ Qimeng Zhang, Wensheng Yu. #RocqProver #ITP #Math
• A formal proof of Stirling’s formula. ~ Yasushige Watase. #Mizar #ITP #Math
• Case study: Saturations as explicit models in equational theories. ~ Mikoláš Janota, Michael Rawson, Stephan Schulz. #ATP #Vampire
• Proof assistants in the age of AI. ~ Leonardo de Moura. #AI4Math #ITP
• Mathematics and machine creativity: A Survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. #AI4Math #ITP
• #Exercitium: Matriz zigzagueante. #Haskell #FunctionalProgramming #Math