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

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

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

• Lecturas compartidas el 4 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La congruencia módulo 2 es una relación de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones con inversa por la izquierda son inyectivas". #ITP #Lean4 #IsabelleHOL #Math
• The Stone-Cech compactification (in Isabelle/HOL). ~ Mike Stannett. #ITP #IsabelleHOL #Math

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

• Lecturas compartidas el 2 de junio de 2024. #ITP #Lean4 #FunctionalProgramming #Haskell #TypeTheory #AI
• Libro "Calculemus (Demostraciones con Lean4)" (versión 2-junio-24). #ITP #Lean4 #Math

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

• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (2-junio-24). #ITP #Lean4 #IsabelleHOL #Math
• Intro to Lean 4: A language at the intersection of programming and mathematics. ~ Kiiya. #ITP #Lean4
• A boolean is maybe true. ~ Håkon Robbestad Gylterud. #FunctionalProgramming #Haskell
• Principles of dependent type theory. ~ Carlo Angiuli and Daniel Gratzer (@danielgratzer@mathstodon.xyz). #TypeTheory #FunctionalProgramming
• L’intelligence artificielle : Hier, aujourd’hui … et demain. ~ Jean-Paul Haton. #IA

Las lecturas compartidas en Mastodon el 31 de mayo de 2024 son

• Lecturas compartidas el 30 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ". #ITP #Lean4 #IsabelleHOL #Math
• Liquid Haskell through the compilers. ~ Facundo Domínguez. #FunctionalProgramming #LiquidHaskell

Las lecturas compartidas en Mastodon el 30 de mayo de 2024 son

• Lecturas compartidas el 29 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y". #ITP #Lean4 #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Formalization of asymptotic convergence for stationary iterative methods. ~ Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin. #ITP #Coq #Math
• Certification of tail recursive bubble–sort in Theorema and Coq. ~ Isabela Dramnesc, Tudor Jebelean, and Sorin Stratulat. #ITP #Coq #Theorema
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk. #ATP #Prover9
• Automated theorem proving for Prolog verification. ~ Fred Mesnard, Thierry Marianne and Etienne Payet. #ATP #Vampire #TPTP #Prolog
• Free foil: Generating efficient and scope-safe abstract syntax. ~ Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. #FunctionalProgramming #Haskell
• Automated theorem provers help improve large language model reasoning. ~ Lachlan McGinness and Peter Baumgartner. #LLMS #ATP

Las lecturas compartidas en Mastodon el 29 de mayo de 2024 son

• Lecturas compartidas el 27 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Autoformalisation #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La paradoja del barbero". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Descomposiciones triangulares. #Haskell #Python #Matemáticas
• IsarMathLib 1.30.0: Modules and update to Isabelle2024. #ITP #Isabelle #Math