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