The readings shared in Bluesky on 25 May 2026 are:

• Four–in-a-row in Rocq. ~ Laurent Théry. #RocqProver #ITP
• Advancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et als. #AI4Math #LeanProver
• An OpenAI model has disproved a central conjecture in discrete geometry. #AI4Math
• Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. #AI4Math #RocqProver
• Tao's equational proof challenge accepted (technical report). ~ Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule. #ATP #AI4Math
• Using Aristotle API for AI-assisted theorem proving in Lean 4: A formalisation case study of the Grasshopper problem. ~ Gabriel Rongyang Lau. #AI4Math #LeanProver #ITP
• The verification problem. ~ Alexander R. Korbonits. #AI4Math
• #Calculemus: Demostraciones con Lean 4 de "Si aₙ converge a L, entonces 2aₙ converge a 2L". #LeanProver #Math
• #RetoLean4: Demostrar con Lean 4 que si aₙ converge a L, entonces 2aₙ converge a 2L. #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 2 (Demostrar con Lean 4 que la sucesión 1, -1, 1, -1,… no es convergente). #LeanProver #ITP #Math
• Reseña de «An OpenAI model has disproved a central conjecture in discrete geometry». #AI4Math
• Reseña de «Advancing mathematics research with AI-driven formal proof search». #AI4Math #LeanProver