The readings shared in Bluesky on 11 June 2025 are

• LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. #ITP #LeanProver #Math #AIforMath #Teaching
• Common Lean pitfalls. ~ Niels Voss. #ITP #LeanProver
• Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library. ~ Brenda Potts. #ITP #LeanProver #RustLang
• Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. #Logic #SMT #Z3 #Teaching
• Martin Davis: An overview of his work in logic, computer science, and philosophy. ~ Liesbeth De Mol, Yuri V. Matiyasevich, Eugenio G. Omodeo, Alberto Policriti, Wilfried Sieg, Elaine J. Weyuker. #Logic #Math #CompSci
• El futuro del razonamiento matemático: Integrando IA y Lean. #IA #ITP #LeanProver #Math #AIforMath
• Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. #ITP #LeanProver #Math #AIforMath #Teaching