The readings shared in Bluesky on 4 May 2026 are:

• Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw et als. #LeanProver #ITP #Math
• Primitive pythagorean triples in lean and reduction modulo odd prime powers. ~ Luke Biddle. #LeanProver #Math
• Sobre la demostración del Problema #1196 de Erdős por GPT-5.4 Pro. ~ Francisco R. Villatoro. #LeanProver #AI4Math
• Nagata factoriality (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• The algebra of iterative constructions (in Isabelle/HOL). ~ Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, Todd Schmid. #IsabelleHOL #ITP
• Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. #Agda #ITP #HoTT
• A monadic implementation of functional logic programs. ~ Michael Hanus, Kai-Oliver Prott, Finn Teegen. #Haskell #FunctionalProgramming
• Arboretum.hs: Symbolic manipulation for algebras of graphs. ~ Eugen Bronasco, Jean-Luc Falcone, Gilles Vilmart. #Haskell #FunctionalProgramming
• Why I still reach for Scheme and Lisp instead of Haskell. ~ Josep Bigorra. #Haskell #Scheme #Lisp #FunctionalProgramming
• Collatz conjecture in Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• CKKS — Polynomials, the canonical embedding, and encoding. ~ Jeremy Kun. #Python #Programming #Math
• MathDuels: a self-play benchmark for mathematical reasoning. ~ Rabdos. #AI4Math
• MathDuels: Evaluating LLMs as problem posers and solvers. ~ Zhiqiu Xu, Shibo Jin, Shreya Arya, Mayur Naik. #AI4Math