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 #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