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

• Lecturas compartidas el 5 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si el límite de la sucesión uₙ es a, entonces el límite de -uₙ es -a". #ITP #Lean4 #IsabelleHOL #Math
• Finding facts in large formalization libraries: Two Isabelle/AFP attempts. ~ Fabian Huch, Yiannos Stathopoulos. #ITP #IsabelleHOL
• Bundling in dependent type theory. ~ Anne Baanen. #ITP #Lean4
• The HOL Light library of formalized mathematics. ~ Marco Maggesi. #ITP #HOL_Light #Math