The readings shared in Bluesky on 19 December 2025 are:

• Proof engineering for program logics in Isabelle/HOL. ~ Chelsea L. Edmonds. #ITP #IsabelleHOL
• Modular proofs in Isabelle/HOL. ~ Chelsea L. Edmonds. #ITP #IsabelleHOL
• Prediction: AI will make formal verification go mainstream. ~ Martin Kleppmann. #AI #LLMs #ITP #LeanProver #IsabelleHOL #Rocq
• Mathematics in the age of Large Language Models. ~ Przemyslaw Chojecki. #AI #Math
• Advancing mathematics research with generative AI. ~ Lisa Carbone. #AI #Math #ITP #LeanProver
• El triángulo de Pascal y las ternas pitagóricas. ~ Miguel Ángel Morales. #Matemáticas