The readings shared in Bluesky on 16 October 2025 are:

• Most proofs are trivial. ~ Lawrence Paulson. #Math #ITP #IsabelleHOL
• An introduction to formal real analysis (Lecture 11: The real numbers I). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Automated Lean proofs for every type. ~ Elizaveta Pertseva. #ITP #LeanProver
• Mathematics with large language models as provers and verifiers. ~ Hieu Le Duc, Leo Liberti. #AI #Math #LLMs #ITP #LeanProver
• Creating a database of motivated proofs. ~ Timothy Gowers. #AI #Math
• Computing is indeed a discipline in crisis. ~ Moshe Vardi. #CompSci
• Libro «Exercitium: Ejercicios de programación funcional con Haskell (Volumen 1: curso 2013–14)». #Haskell #ProgramaciónFuncional #Matemáticas