The readings shared in Bluesky on 12 January 2025 are

• Readings shared January 11, 2025. #ITP #LeanProver #Coq #Rocq #Agda #FunctionalProgramming #Haskell #Python #Math #CategoryTheory #ComputerSci #Education #GenAI
• Prouver que π est irrationnel avec MathComp-Analysis. ~ Reynald Affeldt. #ITP #Coq #Rocq #Math
• Reconciling impredicative axiom and universe. ~ Stefan Monnier. #ITP #Coq #Rocq #HoTT
• Vers une automatisation de la certification des propriétés de clôture pour Prolog. ~ Thierry Marianne, Fred Mesnard, Etienne Payet. #Prolog #LogicProgramming #LPTP
• Why I chose Common Lisp. ~ Dan's Musings. #CommonLisp
• Common Lisp community survey 2024 results. ~ Dan Haskin. #CommonLisp
• Common Lisp. #CommonLisp