The readings shared in Bluesky on 29 May 2026 are:

• A Rust-to-Lean verification pipeline with AI provers: an experience report. ~ Natalia Klaus, Palina Tolmach, Juan Conejero. #LeanProver #ITP
• Agentic proving for program verification. ~ Alessandro Sosso, Akhil Arora, Bas Spitters. #LeanProver #ProgramVerification
• Classification and deontic explosion for contrary-to-duty obligations. ~ Bjørn Kjos-Hanssen. #LeanProver #Logic
• Formalization of commutative algebra and algebraic number theory. ~ Madison Crim. #LeanProver #Math
• Lean companion to Axler's "Linear algebra done right". ~ Rado Kirov. #LeanProver #ITP #Math
• Self-correcting gossip protocols. ~ Giorgio Cignarale, Hans van Ditmarsch, Stephan Felber, Malvin Gattinger, Hugo Rincon Galeana, Vaishnavi Sundararajan. #LeanProver
• Diophantine equations over Z: Universal bounds and parallel formalization. ~ Jonas Bayer, Marco David, Malte Hassler, Yuri Matiyasevich, Dierk Schleicher. #IsabelleHOL #ITP #Math
• The classical Seifert–van Kampen theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos , David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Four paradoxes and a proof assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library. ~ Bernardo Alonso. #CoqProver #ITP #Math
• ATLAS - Autoformalized Textbook Library At Scale. #AI4Math #LeanProver #ITP
• Formalizing mathematics at scale. ~ Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat, Julia Kempe, Remi Munos, Charles Arnal, Vivien Cabannes. #AI4Math #LeanProver #ITP
• Keep the proof state live: Snapshotting for efficient tactic search in Lean 4. #AI4Math #LeanProver
• MathGames: una plataforma de juegos y laboratorios matemáticos donde el aprendizaje se convierte en una experiencia divertida y retadora. #Math