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

• Lecturas compartidas el 14 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #CompSci #Haskell #FunctionalProgramming #Algorithms #AI
• Story of your lazy function’s life (A bidirectional demand semantics for mechanized cost analysis of lazy programs). ~ Li-Yao Xia et als. #ITP #Rocq_Prover
• An evaluation benchmark for autoformalization in Lean4. ~ Aryan Gulati, Devanshu Ladsaria, Shubhra Mishra, Jasdeep Sidhu, Brando Miranda. #Autoformalization #LLMs #ITP #Lean4 #Math
• What does = mean? Mathematicians aren't sure (and that could be a problem). ~ Katie Spalding (@supermathskid). #Math

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

• Lecturas compartidas el 13 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones con inversa son biyectivas". #ITP #Lean4 #IsabelleHOL #Math
• Data structures and algorithms, correctly. ~ Jeremy Siek (@jeremysiek@types.pl). #Algorithms #FunctionalProgramming #ITP #Deduce
• Deduce: A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs. ~ Jeremy Siek (@jeremysiek@types.pl). #Algorithms #FunctionalProgramming #ITP #Deduce
• Formalizing Coppersmith's method (in Isabelle/HOL). ~ Katherine Kosaian, Yong Kiam Tan. #ITP #IsabelleHOL #Math
• Computation, AI and the future of mathematics. ~ David H Bailey. #Math #CompSci #ITP #AI
• The Haskell Unfolder Episode 27: Duality. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming
• The rise of the AI co-pilot: Lessons for design from aviation and beyond (Building on cross-disciplinary insights to shape the future of human-AI interaction). ~ Abigail Sellen, and Eric Horvitz. #AI

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

• Lecturas compartidas el 12 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones suprayectivas tienen inversa por la derecha". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 11 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #ATP #TPTP #FunctionalProgramming #Haskell #OCaml
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones con inversa por la derecha son suprayectivas". #ITP #Lean4 #IsabelleHOL #Math
• Libro "Piensa en Haskell y en Python" (versión del 12-jun-24). #Haskell #Python #Matemáticas #Algorítmica
• El mes de mayo en Exercitium (Ejercicios con Haskell y Python). #Haskell #Python #Matemáticas #Algorítmica
• Formally verified approximate policy iteration. ~ Maximilian Schäffeler, Mohammad Abdulaziz. #ITP #IsabelleHOL #Math

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