The readings shared in Bluesky on 25 November 2025 are:

• Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras. #ITP #LeanProver
• REAL-Prover: Retrieval augmented lean prover for mathematical reasoning. ~ Ziju Shen et als. #ITP #LeanProver #LLMs #Math
• MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs
• Software never fails. ~ kqr. #Programming
• #Exercitium: Expresiones aritmética normalizadas. #Haskell #ProgramaciónFuncional #Matemáticas