Lecturas compartidas el 3 de abril de 2024

#ITP #LeanProver #IsabelleHOL #Coq #HOL4 #Haskell #LogicProgramming #Prolog #Python #Logic #Math #AI #LLMs #Autoformalization

Buenos días

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

• Lecturas compartidas el 2 de abril de 2024. #ATP #Coq #Haskell #ITP #IsabelleHOL #Lean4 #LeanProver #Logic #Math #Pythonl

• Libro "Piensa en Haskell y en Python" (versión del 2-abr-24). #Haskell #Python #Matemáticas #Algorítmica

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

• Broadcast Psi-calculi (in Isabelle/HOL). ~ Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber. #ITP #IsabelleHOL

• Enhancing formal theorem proving: A comprehensive dataset for training AI models on Coq code. ~ Andreas Florath. #ITP #Coq #LLMs

• Improving the Diproche CNL through autoformalization via Large Language Models. ~ Merlin Carl. #ITP #Diproche #LLMs

• A formal proof of R(4,5)=25. ~ Thibault Gauthier, Chad E. Brown. #ITP #HOL4 #Math

• Using large language models for (de-)formalization and natural argumentation exercises for beginner's students. ~ Merlin Carl. #LLMs #Autoformalization #Logic

• AI Mathematical Olympiad – Progress Prize Competition now open. ~ Terence Tao (@tao@mathstodon.xyz). #AI #Math

• Generative logic, teaching Prolog in art & design. ~ Christian Jendreiko. #Prolog #LogicProgramming

También están en GitHub.

Saludos, José A.

---

"Hay que huir de la tristeza, hermana gemela del tedio, pues nos priva de todos los placeres." ~ Erasmo de Róterdam (1466-1536).