The readings shared in Bluesky on 13 February 2025 are

• Is mathematics obsolete? ~ Jeremy Avigad. #Math #ITP #LeanProver #AI #LLMs
• A Coq formalization of unification modulo exclusive-or. ~ Yichi Xu, Daniel J. Dougherty, Rose Bohrer. #ITP #Coq
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• A proof of Hilbert basis theorem and an extension to formal power series (in Isabelle/HOL). ~ Benjamin Puyobro, Benoît Ballenghien, Burkhart Wolff. #ITP #IsabelleHOL #Math
• Why Amazon is betting on 'automated reasoning' to reduce AI's hallucinations. ~ Belle Lin. #AI #LLMs #ITP
• On LLM-generated logic programs and their inference execution methods. ~ Paul Tarau. #LLMs #LogicProgramming #Prolog
• LP-LM: No hallucinations in question answering with logic programming. ~ Katherine Wu, Yanhong A. Liu. #LLMs #LogicProgramming #Prolog
• Improving autoformalization using type checking. ~ Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut. #Autoformalization #LLMs #ITP #LeanProver #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper et als. #LLMs #Math
• A model for learning-curve estimation in efficient neural architecture search and its application in predictive health maintenance. ~ David Solís-Martín, Juan Galán-Páez, Joaquín Borrego-Díaz. #AI
• 50 years of programming language evolution through the software Heritage looking glass. ~ Adèle Desmazières, Roberto Di Cosmo, Valentin Lorentz. #Programming