Las lecturas compartidas en Mastodon el 9 de agosto de 2024 son

• Lecturas compartidas el 8 de agosto de 2024. #ITP #Lean4 #IsabelleHOL #Math #DeepLearning
• A tricky lower bound proof. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Verified transformations for convex programming. ~ Ramon Fernández Mir. #ITP #Lean4 #Math
• First steps towards computational polynomials in Lean. ~ James Harold Davenport. #ITP #LeanProver #Math
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner & Detlef Plump. #ITP #IsabelleHOL
• Validation of a formal floating-point model for the interactive proof assistant Isabelle/HOL. ~ Olof Lindström. #ITP #IsabelleHOL
• Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. #ITP #HOL4
• An in-context learning agent for formal theorem-proving. ~ Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri. #LLMs #ITP #Coq #LeanProver
• Competitive programming in Haskell: Tree path decomposition, part II. ~ Brent Yorgey (@byorgey@mathstodon.xyz). #Haskell #FunctionalProgramming
• typedKanren: Statically typed relational programming with exhaustive matching in Haskell. ~ Nikolai Kudasov & Artem Starikov. #Haskell #FunctionalProgramming
• Combinatorial and algorithmic mathematics (From foundation to optimization) ~ Baha M. Alzalg #Math
• Intelligent Computer Mathematics (17th International Conference, CICM 2024, Proceedings) #ITP #Math
• The potential for AI in science and mathematics. ~ Terence Tao. #IA #Math #ITP #LeanProver