The readings shared in Bluesky on 19 May 2026 are:

• A shallow dive into formal verification. ~ Vitalik Buterin. #LeanProver #ITP
• Decidable (Logic in Lean). #LeanProver #ITP #FunctionalProgramming
• LeanBET: Formally-verified surface area calculations in Lean. ~ Ejike D. Ugwuanyi, Colin T. Jones, John Velkey, Tyler R. Josephson. #LeanProver #ITP #Math
• TableauxRocq: A deep embedding of free-variable tableaux in Rocq. ~ Johann Rosain, Julie Cailler. #RocqProver #ITP
• From LLM-generated conjectures to Lean formalizations: automated polynomial inequality proving via sum-of-squares certificates. ~ Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang. #AI4Math #LeanProver #ITP
• Lean meets theoretical computer science: scalable synthesis of theorem proving challenges in formal-informal pairs. ~ Terry Jingchen Zhang et als. #AI4Math #LeanProver #ITP
• #RetoLean4: Demostrar con Lean 4 que la sucesión 1, -1, 1, -1, … no es convergente. #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 1 (Demostrar con Lean 4 que la sucesión 1/n converge a 0). #LeanProver #ITP #Math