The readings shared in Bluesky on 13 May 2025 are

• Course: Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #ITP #LeanProver #FunctionalProgramming
• Formalizing a proof in Lean using Github copilot and canonical. ~ Terence Tao. #ITP #LeanProver #Math
• APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. ~ Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh. #LLMs #ITP #LeanProver
• La gran ilusión de la IA: no piensa, no siente, pero habla como si lo hiciera. ~ Ramón López de Mántaras. #IA