The readings shared in Bluesky on 20 October 2025 are:

• Formalizing Wigner’s semicircle law in Lean. ~ Haoyan Jiang et als. #ITP #LeanProver #Math
• Towards verifying the "Three amigos". ~ Carl Kwan. #ITP #ACL2 #Math
• Pelletier’s problem 24 in Mizar. ~ Alex Nelson. #ITP #Mizar #Logic #Math
• ProofBridge: Auto-formalization of natural language proofs in Lean via joint embeddings. ~ Prithwish Jana et als. #ITP #LeanProver #Autoformalization #LLMs #Math
• Spatial DP: Finding the largest square. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Divisibles por el primero. #Haskell #ProgramaciónFuncional #Matemáticas