The readings shared in Bluesky on 29 July 2025 are

• Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. #FormalVerification #ProofAssistants #CoqProver
• Symbolic world models in Lean 4 for reinforcement learning. ~ Matěj Kripner. #ITP #LeanProver #MachineLearning
• Formal verification of the safegcd implementation. ~ Russell O'Connor, Andrew Poelstra. #FormalVerification #ProofAssistants #CoqProver
• Formal verification of pairing heaps in Rocq. ~ Cosmin-Ionut Visan. #FormalVerification #ProofAssistants #Rocq
• Verified functional graph algorithms using the Rocq prover (Coq). ~ Leopold Frieberger. #FormalVerification #ProofAssistants #Rocq
• Formal verification of leftist and skew heaps in Rocq. ~ Elena Marcela Dumitrache. #FormalVerification #ProofAssistants #Rocq
• Comparing codes: Spiral matrix (another matrix layer problem). ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO
• #Exercitium: Problemas de programación con Haskell (noviembre de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (julio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas