The readings shared in Bluesky on 10 May 2025 are

• A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. #ITP #Python #Math
• How to (actually) prove it - New frontiers of mathematics & computing in Lean. ~ Kiran. #ITP #LeanProver #Math
• LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. #ITP #LeanProver #Mathlib
• How do undergraduates do mathematics? (A guide to studying mathematics at Oxford University). #Math