Las lecturas compartidas en Mastodon el 4 de junio de 2024 son

• Lecturas compartidas el 3 de junio de 2024. #ITP #Lean4 #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si uₙ está acotada y el límite de vₙ es 0, entonces el límite de uₙ·vₙ es 0". #ITP #Lean4 #IsabelleHOL #Math
• Sorted terms (in Isabelle/HOL). ~ Akihisa Yamada, and René Thiemann. #ITP #IsabelleHOL
• Verifying a decision procedure for pattern completeness (in Isabelle/HOL). ~ René Thiemann, and Akihisa Yamada. #ITP #IsabelleHOL
• Countable sums and discrete (sub)distributions (in Isabelle/HOL). ~ Gergely Buday, and Andrei Popescu. #ITP #IsabelleHOL #Math