The readings shared in Bluesky on 5 June 2025 are

• Exceptional set in the abc conjecture (in Lean). ~ Jared Duker Lichtman, Bhavik Mehta. #ITP #LeanProver #Math
• IDE for validating specifications. ~ Evan Miyazono, Daniel Windham, Alexandre Rademaker. #ITP #LeanProver
• Faithful logic embeddings in HOL — Deep and shallow (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• A verified reduction algorithm from MLSSmf to MLSS. ~ Yiran Duan, Lukas Stevens. #ITP #IsabelleHOL #Math
• David Poole on knowledge graphs and relational learning. #AI #LogicProgramming
• IA y matemáticas (presente y futuro). #IA #Matemáticas