Lecturas compartidas el 19 de marzo de 2024
#CategoryTheory #Coq #ITP #IsabelleHOL #LLMs #LeanProver #LeanProver #Math #Programming
Buenos días
Las lecturas compartidas en Mastodon el 19 de marzo de 2024 son
Lecturas compartidas el 18 de marzo de 2024. #AI #ATP #Coq #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LLMs #Lean4 #LeanProver #MachineLearning #Math #ProofAssistants
An Isabelle/HOL formalization of narrowing and its applications to E-unifiability, reachability and infeasibility. ~ Dohan Kim. #ITP #IsabelleHOL
Llemma: An open language model for mathematics. ~ Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, Sean Welleck. #LLMs #Math #ITP #LeanProver #IsabelleHOL #Coq
Can AI do mathematics? ~ Kevin Buzzard. #ITP #Math #LeanProver via Pietro Monticone (@PietroMonticone).
What is an interactive theorem prover? ~ Kevin Buzzard. #ITP #Math #LeanProver via Pietro Monticone (@PietroMonticone).
The Liquid Tensor Experiment. ~ Kevin Buzzard. #ITP #Math #LeanProver via Pietro Monticone (@PietroMonticone).
Bugs in Large Language Models generated code: An empirical study. ~ Florian Tambon, Arghavan Moradi Dakhel, Amin Nikanjam, Foutse Khomh, Michel C. Desmarais, Giuliano Antoniol. #LLMs #Programming
Category theory inspired by LLMs. ~ Tai-Danae Bradley. #LLMs #CategoryTheory
También están en GitHub.
Saludos, José A.
"Un alma triste puede matarte más rápido, mucho más rápido, que un germen." ~ John Steinbeck (1902-1968).
