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. ~ Balazs Toth, Martin Desharnais-Schäfer, Jasmin Blanchette. #ITP #IsabelleHOL
• Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #LeanProver #FunctionalProgramming #ITP
• Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. #ITP #RocqProver
• Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies- #ITP #RocqProver
• Computation-tree semantics: An algorithmic approach to structurally defined relations. ~ Sean Kristian Remond Harbo, Hans Hüttel. #ITP #RocqProver
• Formal verification for JavaScript regular expressions: A proven mechanized semantics and its applications. ~ Aurèle Barrière, Victor Deng, Clément Pit-Claudel. #ITP #RocqProver
• 130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. #ITP #Mizar #LLMs #Math #Autoformalization
• Using AI, mathematicians find hidden glitches in fluid equations. ~ Charlie Wood. #AI #Math
• #Exercitium: Números naturales separados por ceros. #Haskell #FunctionalProgramming #Math