Readings shared December 29, 2025
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