Readings shared May 19, 2026
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