The readings shared in Bluesky on 1 May 2025 are

• DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. ~ Z.Z. Ren et als. #LLMs #ITP #LeanProver
• Mathematical beauty, truth and proof in the age of AI. ~ Jordana Cepelewicz. #Math #AI #ITP
• Logical modelling in CS education: Bridging the natural language gap. ~ Tristan Kneisel, Fabian Vehlken, Thomas Zeume. #Logic #Education
• Iltis: An interactive, web-based system for teaching formal foundations of computer science. #Logic #Education
• Introduction to Iltis: An interactive, web-based system for teaching logic. ~ Gaetano Geck et als. (2018). #Logic #Teaching
• Iltis: Learning Logic in the Web. ~ Gaetano Geck et als. (2022). #Logic #Teaching
• Clear: A formal verification framework for smart contracts in Lean. ~ Julian Sutherland. #ITP #LeanProver