The readings shared in Bluesky on 21 June 2026 are:

• A Lean 4 formalization of euclidean domain algorithms from a 1986 icon experimentation package. ~ Lars Warren Ericson. #LeanProver #ITP #Math
• A Lean-certified proof of K₈(4, 2) = 23. ~ Andreas Florath. #LeanProver #ITP #Math
• EconCSLib: A Lean library for computational economics and AI-Assisted research. ~ Xiaohui Bei, Jiajun Ma, Zhan Jing, Hongfei Fu, Zhihao Gavin Tang. #LeanProver #ITP
• Finishing Oltean's completeness proof in Lean 4 for hybrid logic L(∀). ~ Lars Warren Ericson. #LeanProver #ITP #Logic
• Formalizing chip-firing and Riemann-Roch for graphs in Lean 4. ~ Dhyey Dharmendrakumar Mavani, Nathan Pflueger. #LeanProver #ITP
• Formalizing extended complex numbers, Mobius transformations, and cross ratio in Lean 4. ~ Fubin Yan, Kenneth W. Shum. #LeanProver #ITP #Math
• Prismriver: Formalization of music theory and algorithmic composition in Lean 4. ~ Leni Aniva, Claire Wang. #LeanProver #ITP
• Formalizing numerical analysis: an agent pipeline and quality audit beyond kernel acceptance. ~ Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess, Vasily Ilin. #AI4Math #LeanProver #ITP
• A formalization of the exponential blowup in the transformations between CNF and DNF (in Isabelle/HOL). ~ Leon Raffael Schulz, Martin Desharnais-Schäfer, Jan Johannsen. #IsabelleHOL #ITP
• Formalization of countable multisets (in Isabelle/HOL). ~ Mathias Schack Rabing, Dmitriy Traytel. #IsabelleHOL #ITP
• Formalization of weighted sets (in Isabelle/HOL). ~ Mathias Schack Rabing, Dmitriy Traytel. #IsabelleHOL #ITP
• LLMemma: An LLM-guided Isabelle proof synthesis system. ~ Daniel Busing, Hyunkyung Lee, Isaac Mangano, Timothy Stanbrough, Tommy Tran. #IsabelleHOL #ITP #LLMs
• The Dottie number (in Isabelle/HOL). ~ Lawrence C. Paulson. #IsabelleHOL #ITP #Math
• The detour calculus: Rigorous local deformation of integration contours. ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness. ~ Karen Sargsyan. #Agda #ITP
• Programmable record types in Haskell. ~ Arthur Jamet, Michael Vollmer. #Haskell #FunctionalProgramming
• Sheaves in Haskell. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Writing static checks to an unsuspecting library with Liquid Haskell. ~ Xavier Góngora. #Haskell #FunctionalProgramming
• Writing Prolog with ChatGPT. ~ John D. Cook. #Prolog #LogicProgramming #ChatGPT+ #RetoLean4: Propuesta del reto 6 (Demostrar el teorema del emparedado: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L). #LeanProver #ITP #Math
• #RetoLean4: Propuesta del reto 7 (Demostrar que la composición de funciones inyectivas es inyectiva). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 5 (Demostrar que 5²ⁿ - 2³ⁿ es divisible por 17). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 6 (Demostrar el teorema del emparedado: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L). #LeanProver #ITP #Math