Lecturas compartidas el 12 de abril de 2024

#ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Math #IMO #AI #NeuralNetwork #Emacs #OrgMode

Buenos días

Las lecturas compartidas en Mastodon el 12 de abril de 2024 son

• Lecturas compartidas el 11 de abril de 2024. #Prolog #LogicProgramming #Math

• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL: "f[s ∩ t] ⊆ f[s] ∩ f[t]". #ITP #LeanProver #Lean4 #IsabelleHOL #Matemáticas

• Wu's method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists at IMO geometry. ~ Shiven Sinha et als. #AI #ATP #IMO #Math

• Coq tactics in plain english. ~ Charles Averill. #ITP #Coq

• Formal program verification (Rigorous proof of program correctness and security). ~ Charles Averill. #ITP #Coq

• Ann: ob-coq (A package for Coq developments in Org Mode). ~ Michael Herstine (@unwoundstack). #ITP #Coq #Emacs #OrgMode

• Dyadic Decomposition using Functional lenses. ~ Eduardo Lemos. #Haskell #FunctionalProgramming

• Solving Advent of Code ’23 “Aplenty” by Compiling. ~ Abhinav Sarkar (@abnv@fantastic.earth). #Haskell #FunctionalProgramming

• Neural networks for mathematical reasoning: Evaluations, capabilities, and techniques. ~ Yuhuai Tony Wu. #NeuralNetwork #Reasoning #Math

• Epsilon: Scientific research at your fingertips (Epsilon uses AI to answer research questions with academic literature). #AI

También están en GitHub.

Saludos, José A.

---

"No hay cosas sin interés. Tan sólo personas incapaces de interesarse." ~ G.K. Chesterton (1874-1936).