Lecturas compartidas el 22 de abril de 2024
#ITP #Lean4 #IsabelleHOL #Coq #Agda #FunctionalProgramming #Haskell #Nix #Math #IMO
Buenos días
Las lecturas compartidas en Mastodon el 22 de abril de 2024 son
Lecturas compartidas el 21 de abril de 2024. #ITP #Lean4 #IsabelleHOL #Math #CategoryTheory #AI #LLMs
#Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "f[s ∪ f⁻¹[v ⊆ f[s] ∪ v"]]. #ITP #Lean4 #IsabelleHOL #Math
Using the proof assistant Lean in undergraduate mathematics classrooms. ~ Brendan Larvor, Gila Hanna, Xiaoheng Yan. #ITP #Lean4 #Math
Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin. #ITP #Coq #Math
Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw (@david@social.wub.site) et als. #ITP #Lean4 #Math #IMO
Lean 99: Ninety-nine Lean problems. ~ Kitamado. #FunctionalProgramming #Lean4
Getting your Haskell executable statically linked with Nix. ~ Tom Sydney Kerckhove. #FunctionalProgramming #Haskell #Nix
A note about coercions. ~ Oleg Grenrus (@phadej). #FunctionalProgramming #ITP #Agda
También están en GitHub.
Saludos, José A.
"El descanso, la naturaleza, los libros, la música… tal es mi idea de la felicidad." ~ León Tolstói (1828-1910).
