Lecturas compartidas el 15 de abril de 2024
#ITP #Lean4 #IsabelleHOL #Coq #PVS #FunctionalProgramming #Haskell #Math #AI #Education
Buenos días
Las lecturas compartidas en Mastodon el 15 de abril de 2024 son
Lecturas compartidas el 14 de abril de 2024. #ITP #Lean4 #Mathlib
#Calculemus: Demostraciones con Lean4 e Isabelle/HOL: "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]". #ITP #LeanProver #Lean4 #IsabelleHOL #Matemáticas
Large-scale formal proof for the working mathematician (lessons learnt from the ALEXANDRIA project). ~ Lawrence C. Paulson.f#page=17 #ITP #IsabelleHOL #Math
Evasiveness through Binary Decision Diagrams. ~ Jesús Aransay, Laureano Lambán, Julio Rubio.f#page=49 #ITP #IsabelleHOL
Category theory in Isabelle/HOL as a basis for meta-logical investigation. ~ Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott.f#page=81 #ITP #IsabelleHOL
Isabelle formalisation of original representation theorems. ~ Marco B. Caminati.f#page=110 #ITP #IsabelleHOL #Math
Formalization quality in Isabelle. ~ Fabian Huch, Yiannos Stathopoulos.f#page=154 #ITP #IsabelleHOL
Formalizing free groups in Isabelle/HOL: The Nielsen-Schreier theorem and the conjugacy problem. ~ Aabid Seeyal Abdul Kharim et als. #ITP #IsabelleHOL #Math
Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method. ~ Mohit Tekriwal et als. #ITP #Coq #Math
Multiple-inheritance hazards in dependently-typed algebraic hierarchies. ~ Eric Wieser. #ITP #LeanProver
Nominal AC-matching. ~ Mauricio Ayala-Rincón et als.f#page=65 #ITP #PVS
CoProver: A recommender system for proof construction. ~ Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar. #ITP #PVS
From foundations to frontiers: Mastering Haskell programming. ~ Byte Sorcery. #Haskell #FunctionalProgramming
AI for Math resources. ~ Talia Ringer et als. #AI #Math
Reimagining middle school education: The synergy of AI and Montessori principles (Next-level AI curriculum development). ~ Nick Potkalitsky, Sam Bobo. #AI #Education
También están en GitHub.
Saludos, José A.
"Me rebelo contra la vieja mentira de que la mayoría siempre tiene la razón." ~ Henrik Ibsen (1828-1906).