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

• Lecturas compartidas el 10 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones inyectivas tienen inversa por la izquierda". #ITP #Lean4 #IsabelleHOL #Math
• The Lévy-Prokhorov metric (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• The Riesz representation theorem (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• The new TPTP format for interpretations. ~ Geoff Sutcliffe, Alexander Steen, Pascal Fontaine. #ATP #TPTP
• Ranking functional programming languages (Why I'm biased and excited). #FunctionalProgramming #Haskell #Scala #OCaml #PureScript #Elm #Roc #Unison #Gleam #Fsharp

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

• Lecturas compartidas el 9 de junio de 2024. #ITP #Lean4 #Math #AI
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si g ∘ f es suprayectiva, entonces g es suprayectiva". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Representación de Zeckendorf. #Haskell #Python #Matemáticas
• Formally verified interval arithmetic and its application to program verification. ~ Achim D. Brucker, Teddy Cameron-Burke, Amy Stell. #ITP #IsabelleHOL
• Failing at combinatorics with Haskell. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 8 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Autoformalization #LLMs
• Libro "Calculemus (Demostraciones con Lean4)" (versión 8-junio-24). #ITP #Lean4 #Math
• AI will become mathematicians’ ‘co-pilot’ (Fields Medalist Terence Tao explains how proof checkers and AI programs are dramatically changing mathematics). ~ Christoph Drösser. #AI #ITP #Lean4 #Math

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

• Lecturas compartidas el 7 de junio de 2024. #ITP #Lean4 #IsabelleHOL #PVS #Math #ATP #Prover9 #SMT #Z3 #FunctionalProgramming #Haskell #LLMs
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (8-junio-24). #ITP #Lean4 #IsabelleHOL #Math
• Process-driven autoformalization in Lean 4. ~ Jianqiao Lu et als. #Autoformalization #LLMs #ITP #Lean4
• Announcing a free video-based Haskell introduction course. ~ Andres Löh (@kosmikus@functional.cafe). #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 6 de junio de 2024. #ITP #Lean4 #IsabelleHOL #HOL_Light #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si g ∘ f es inyectiva, entonces f es inyectiva". #ITP #Lean4 #IsabelleHOL #Math
• Mechanized analysis of Anselm's modal ontological argument. ~ John Rushby. #ITP #PVS
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. ~ Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, Kai Chen. #LLMs #ITP #Lean4
• Calculating compilers effectively (Functional Pearl). ~ Zac Garby, Graham Hutton, Patrick Bahr. #FunctionalProgramming #Haskell
• Working towards a more stable Template Haskell. ~ Teo Camarasu. #FunctionalProgramming #Haskell
• Andrew Granville: Accepted proofs: Objective truth, or culturally robust? ~ Gil Kalai. #Math
• A closer look at logical reasoning with LLMs: The choice of tool matters. ~ Long Hei Matthew Lam, Ehsan Shareghi. #LLMs #ATP #Prover9 #SMT #Z3

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