The readings shared in Bluesky on 24 April 2025 are

• On the averaging problem of ideal families related to Frankl's conjecture with formal proof by Lean 4. ~ Masahiro Hachimori, Kenji Kashiwabara. #ITP #LeanProver #Math
• #Exercitium: Sistema factorádico de numeración. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". #LeanProver #IsabelleHOL #Math