The readings shared in Bluesky on 14 December 2025 are:

• A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. #ITP #Rocq
• A modular Lean 4 framework for confluence and strong normalization of lambda calculi with products and sums. ~ Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz, Tiago de Veras. #ITP #LeanProver
• Learning about proof with the theorem prover Lean: the abundant numbers task. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math
• So, computers can prove theorems (in Lean), what’s next? ~ Alex J. Best. #AI #Math #ITP #LeanProver
• Lessons from the PrimeNumberTheorem+ project and real analysis game. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Challenges in (auto)formalizing category theory. ~ Emily Riehl. #ITP #LeanProver #Math
• The making of Lean. ~ Leo de Moura. #ITP #LeanProver
• The Carleson project: formalization and collaboration. ~ Michael B. Rothgang. #ITP #LeanProver
• Differential geometry in Mathlib. ~ Michael B. Rothgang. #ITP #LeanProver
• Brownian motion and stochastic integrals. ~ Rémy Degenne et als. #ITP #LeanProver #Math
• Probability theory in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Math
• The Haskell Unfolder Episode 52: Bidirectional parsing and printing (of JSON). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Desemparejamiento de listas. #Haskell #ProgramaciónFuncional