The readings shared in Bluesky on 13 April 2025 are

• Completeness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. #ITP #IsabelleHOL #Math #SetTheory
• Efficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. #ITP #Coq
• Mathematical reading list (University of Cambridge). #Math
• LLMs can't stop making up software dependencies and sabotaging everything. ~ Thomas Claburn. #AI #LLMs #Programming
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]". #LeanProver #IsabelleHOL #Math
• Curso "Razonamiento automático (2011-12)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL