Lecturas compartidas el 4 de marzo de 2024
Buenos días
Las lecturas compartidas en Mastodon el 4 de marzo de 2024 (sobre IA, verificación formal, Haskell, Isabelle/HOL, Lean, Matemáticas, Python y SMT) son
Cubical categories (in Isabelle/HOL). ~ Georg Struth, Tanguy Massacrier. #ITP #IsabelleHOL
Formally verified mathematics (With the help of computational proof assistants, formal verification could become the new standard for rigor in mathematics). ~ Jeremy Avigad, John Harrison (2014). #ITP #Math
Errors and corrections in the mathematical literature. ~ Joseph F. Grcar (2013). #Math
Whither mathematics? ~ Brian Davies (2005). #Math #ITP
Desperately seeking mathematical truth. ~ Melvyn B. Nathanson (2008). #Math
Generating and exploiting automated reasoning proof certificates. ~ Haniel Barbosa, Clark Barrett et als. (2023) #SMT #FormalVerification
Kevin's all-synth techno band covers Andrew's greatest hit (Part two: what will Lean understand?). ~ Michael Harris. #AI #Math #ITP #LeanProver
También están en GitHub.
Saludos, José A.
"Mejor es modificar nuestros deseos que la ordenación del mundo." ~ René Descartes (1596-1650).
