The readings shared in Bluesky on 9 March 2026 are:

• Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP
• Formalization in Lean of faithfully flat descent of projectivity. ~ Liran Shaul. #LeanProver #ITP
• Formalizing a proof in Lean using Claude Code. ~ Terence Tao. #LeanProver #ITP #AI4Math
• Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. ~ Joseph Tooby-Smith. #LeanProver #ITP #Physics
• Formalizing unstable quasinormal modes and the quantum black hole bomb in Lean 4. ~ Naoki Takata. #ITP #LeanProver
• Implementing dependent type theory inhabitation and unification. ~ Chase Norman, Jeremy Avigad. #LeanProver #ITP
• LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. #LeanProver #ITP #Math #AI4Math
• Mathematicians in the age of AI. ~ Jeremy Avigad. #AI4Math #LeanProver #ITP
• Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. #AI4Math #LeanProver #ITP
• Unbiasing symmetric monoidal categories in Lean. ~ Robin Carlier. #LeanProver #ITP
• Apply2Isar: Automatically converting Isabelle/HOL apply-style proofs to structured Isar. ~ Sage Binder, Hanna Lachnitt, Katherine Kosaian. #IsabelleHOL #ITP
• A topological rewriting of Tarski’s mereogeometry. ~ Richard Dapoigny. #CoqProver #ITP
• Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. #RocqProver #ITP
• The floor is magma. ~ Alexandre Esteves. #Haskell #FunctionalProgramming
• Can the most abstract math make the world a better place? ~ Natalie Wolchover. #CategoryTheory #Math
• Category theory for programming. ~ Benedikt Ahrens, Kobe Wullaert. #CategoryTheory #Haskell #LeanProver #FunctionalProgramming
• Lambda calculus for dummies: The Church encoding. #LambdaCalculus #FunctionalProgramming
• Emacs and Vim in the age of AI. ~ Bozhidar Batsov. #Emacs #AI
• Una introducción a la programación en Emacs Lisp. ~ Robert J. Chassell, David Arroyo Menéndez. #Emacs #Lisp