The readings shared in Bluesky on 22 September 2025 are:

• Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin et als. #ITP #LeanProver
• Computationally-sound symbolic cryptography in Lean. ~ Stefan Dziembowski et als. #ITP #LeanProver
• Formal verification of the Euler Sieve via Lean. ~ Isaac (Rucheng) Li. #ITP #LeanProver #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers (video). ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver #ATP #SMT
• Determination of the fifth Busy Beaver value. ~ Justin Blanchard et als. #ITP #CoqProver #Rocq
• Discovering new theorems via LLMs with in-context proof learning in Lean. ~ Kazumi Kasaura et als. #ITP #LeanProver #Math #LLMs
• Refinement-types driven development: A study. ~ Facundo Domínguez, Arnaud Spiwack. #FunctionalProgramming #Liquid #Haskell #SMT
• Feeling cranky about AI and CS education. ~ Valerie Barr. #AI #CompSci #Education
• AWS scientist: Your AI strategy needs mathematical logic. ~ Byron Cook. #AI #LLMs #Logic #Math #ATP #ITP
• #Exercitium: Producto cartesiano de una familia de conjuntos. #Haskell #ProgramaciónFuncional #Matemáticas