The readings shared in Bluesky on 27 February 2025 are

• Compactness theorem for first-order logic (in Isabelle/HOL). ~ Sophie Tourret, Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
• CuDIP: Enhancing theorem proving in LLMs via curriculum learning-based direct preference optimization. ~ Shuming Shi et als. #AI #LLMs #ATP #Logic #Math
• TheoremExplainAgent: Towards multimodal explanations for LLM theorem understanding. ~ Max Ku et als. #AI #LLMs #ATP #Logic #Math
• ChatGPT vs. DeepSeek: A comparative study on AI-based code generation. ~ Md Motaleb Hossen Manik. #AI #LLMs #Programming