The readings shared in Bluesky on 19 March 2025 are

• A trickier lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. #LLMs #Programming #FormalVerification
• Towards AI-assisted academic writing. ~ Daniel J. Liebling et als. #AI #LLMs
• VisuAlgo: Visualising data structures and algorithms through animation. #Programming #CompSci
• VisuAlgo muestra visualmente cómo funcionan los algoritmos, las estructuras de datos y cómo resolver problemas. ~ @Alvy. #Programación #Computación
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus