The readings shared in Bluesky on 23 June 2025 are

• Formalising differential geometry and topology in Lean: Differential forms and the Whitney–Graustein theorem. ~ Sam J. L. Lindauer. #ITP #LeanProver #Math
• A verified algebra of cognition: A Coq formalization of the distinction field. ~ Andrey Shkursky. #ITP #CoqProver
• A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL
• Towards advanced mathematical reasoning for LLMs via first-order logic theorem proving. ~ Chuxue Cao et als. #LLMs #ITP #LeanProver #Math
• Curso "Informática (2014-15)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima