The readings shared in Bluesky on 29 December 2025 are:

• Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT
• The biggest controversy in maths could be settled by a computer. Alex Wilkins. #ITP #LeanProver #Math
• Report on the current situation surrounding inter-universal Teichmüller theory (IUT). ~ Shinichi Mochizuki. #Math #ITP #LeanProver
• The machine-checked complete formalization of Landau’s foundations of analysis in Rocq. ~ Yue Guan, Yaoshun Fu, Xiangtao Meng. #ITP #Rocq #Math
• Formal verification of Borrow-Checking by local commutation diagrams. ~ Alban Reynaud Michez. #ITP #Rocq
• The unnegatable loop: Tetralemma's performative geometry (with Coq-verification). ~ Siegfried Meister. #ITP #CoqLang
• Une sémantique de Kahn mécanisée pour les machines à états. ~ Timothy Bourke, Paul Jeanmaire, Marc Pouzet. #ITP #Rocq
• Algebraizing higher-order effects. ~ Martin Andrieux, Alan Schmitt. #ITP #Agda
• NAMOR: a new Agda library for modal extended sequents. ~ Riccardo Borsetto, Margherita Zorzi. #ITP #Agda
• Formalisation de la stabilité de l’erreur d’estimation de l’inclinaison d’un robot. ~ Lynda Bentoucha, Reynald Affeldt. #ITP #Rocq
• Tacq: Context aware tactic recommendation for Rocq. ~ Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias, Marc Lelarge, Theo Stoskopf. #ITP #Rocq
• Assignments and strategies in democratic forking analysed with Isabelle/HOL. ~ Jan-Georg Smaus. #ITP #IsabelleHOL
• Dynamic pushdown networks (in Isabelle/HOL). ~ Peter Lammich. #ITP #IsabelleHOL
• Set reconciliation (in Isabelle/HOL). ~ Paul Hofmeier, Emin Karayel. #ITP #IsabelleHOL
• On the design and implementation of Modular Explicits. ~ Samuel Vivien, Didier Rémy, Gabriel Scherer. #OCaml #FunctionalProgramming
• Mapping and explaining syntax errors with LRgrep. ~ Frédéric Bour, François Pottier. #OCaml #FunctionalProgramming
• Cairn : Trouver son chemin dans Menhir. ~ Vincent Penelle. #OCaml #FunctionalProgramming
• Advent of Code 2025: Haskell solution reflections for all 12 days. ~ Justin Le. #Haskell #FunctionalProgramming
• Carnap: a free and open software framework written in Haskell for teaching and studying formal logic. #Haskell #FunctionalProgramming #Logic
• Vibe reasoning: Eliciting frontier AI mathematical capabilities (A case study on IMO 2025 Problem 6). ~ Jiaao Wu, Xian Zhang, Fan Yang, Yinpeng Dong. #AI #Math
• Advice for amateur mathematicians on writing and publishing papers. ~ Henry Cohn. #Math
• #Exercitium: Listas disjuntas. #Haskell #ProgramaciónFuncional #Matemáticas