The readings shared in Bluesky on 24 August 2025 are

• LeanGeo: Formalizing competitional geometry problems in Lean. ~ Chendong Song et als. #ITP #LeanProver #Math #LLMs
• To zip through the cost analysis of probabilistic programs. ~ Matthias Hetzenberger, Georg Moser, Florian Zuleger. #Haskell #FunctionalProgramming
• #Exercitium: Mastermind. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Anagramas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 23 August 2025 are

• Formalizing class field theory. ~ Georgia Harbor-Collins, Mohit Hulse. #ITP #LeanProver #Math
• Decidable equality for indexed data types, take 2. ~ Brent Yorgey. #Agda #FunctionalProgramming #ITP

The readings shared in Bluesky on 22 August 2025 are

• Definite integrals, II: improper integrals. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Continuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda #Math
• Reasoning about weak isolation levels in separation logic. ~ Anders Alnor Mathiasen et als. #ITP #Rocq
• The Baby paradox in Haskell. ~ Justin Le. #Haskell #FunctionalProgramming #Logic
• Applicative-wired monad pattern. ~ Chris Done. #Haskell #FunctionalProgramming
• #Exercitium: Iguales al siguiente. #Haskell #FunctionalProgramming
• #Exercitium: Ordenación por el máximo. #Haskell #FunctionalProgramming
• #Exercitium: La bandera tricolor. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Determinación de los elementos minimales. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 20 August 2025 are

• Queen domination by SAT solving. ~ Taha Rostami, Curtis Bright. #ATP #SAT_Solving
• The price of intelligence (Three risks inherent in LLMs). ~ Mark Russinovich, Ahmed Salem, Santiago Zanella-Béguelin, Yonatan Zunger. #AI #LLMs
• #Exercitium: Problemas de programación con Haskell (noviembre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (octubre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (julio de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2014). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 19 August 2025 are

• Granite: A library for producing terminal plots. It depends only on Haskell's base package so it should be easy to use and install. ~ Michael Chavinda. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell (diciembre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 August 2025 are

• Formalizing axiomatics for first-order logic. ~ Jørgen Villadsen, Simon Tobias Lund, Anders Schlichtkrull. #ITP #IsabelleHOL #Logic
• Formal correctness proofs for efficient CHAD. ~ Benjamin Meijs. #ITP #Agda
• Binary tree BFS: Zigzag order. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Problemas de programación con Haskell (marzo de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (enero de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 17 August 2025 are

• Beyond booleans. ~ Dan Abramov. #ITP #LeanProver
• Counterpart-based quantified temporal logics. ~ Fabio Gadducci, Andrea Laretto, Davide Trotta. #ITP #Agda
• Type soundness of functional languages with subtyping in Lang-n-Prove. ~ Matteo Cimini, Joan Montas. #ITP #Abella
• Invertible syntax without the tuples (Functional Pearl). ~ Mathieu Boespflug, Arnaud Spiwack. #Haskell #FunctionalProgramming
• Understanding Fermat's Last Theorem's proofs. ~ Alex Qiu et als. #Math

The readings shared in Bluesky on 16 August 2025 are

• #Exercitium: Problemas de programación con Haskell (junio de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 15 August 2025 are

• Definite integrals, I: easy cases over finite intervals. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Revisiting the Fast Fourier Transform in Rocq. ~ Laurent Théry. #ITP #Rocq #Math
• The Vampire diary. ~ Filip Bártek et als. #ATP #Vampire
• HaLLMos: Expert-guided AI for learning to write mathematical proofs. #Math #AI
• HaLLMos (IA para aprender a escribir demostraciones matemáticas). #Math #AI
• #Exercitium: Problemas de programación con Haskell (diciembre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (noviembre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (octubre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

HaLLMos es un sistema de inteligencia artificial gratuito diseñado para ayudar en la redacción de pruebas matemáticas de nivel básico. El sistema revisa borradores, identifica lagunas en el razonamiento y facilita el proceso de iteración sin revelar directamente la respuesta.

Es completamente gratuito, funciona desde el navegador web y no requiere crear una cuenta. Los usuarios pueden elegir entre ejercicios introductorios para aprender técnicas de demostración o utilizar el espacio de pruebas libre para trabajar con sus propios problemas.