The readings shared in Bluesky on 7 December 2025 are:

• 50 years of proof assistants. ~ Lawrence Paulson. #ITP #IsabelleHOL #CoqProver #HOL
• DeepWiki leanprover-community/mathlib4: A comprehensive database of formalized theorems in Lean 4. #ITP #LeanProver #Math
• The Seifert-van Kampen theorem via computational paths: A formalized approach to computing fundamental groups. ~ Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. #ITP #LeanProver #Math
• Teaching Prolog and logic programming with Jupyter Notebooks. ~ Galileo Sartor, Adam Wyner. #Prolog #LogicPO
• Functional Python programming in introductory computer science courses. ~ Rajshekhar Sunderraman. #Python #FunctionalProgramming
• #Exercitium: Números que sumados a su siguiente primo dan primos. #Haskell #ProgramaciónFuncional #Matemáticas