Readings shared November 25, 2025
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