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

• Lecturas compartidas el 18 de junio de 2024. #ITP #IsabelleHOL #Math #ATP #SAT #Math #LogicProgramming #Prolog #AI #LLMs #Programming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones biyectivas tienen inversa". #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La equipotencia es una relación reflexiva". #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La inversa de una función es biyectiva". #ITP #Lean4 #IsabelleHOL #Math
• Exploring advanced functional programming techniques in Haskell: Monads, functors, and applicatives. ~ Omid Farhang (@omid@floss.social). #FunctionalProgramming #Haskell
• miniCodeProps: A minimal benchmark for proving code properties. ~ Evan Lohn, Sean Welleck. #LLMs #ITP #Lean4 #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 19 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La equipotencia es una relación simétrica". #ITP #Lean4 #IsabelleHOL #Math
• Transforming optimization problems into disciplined convex programming form. ~ Ramon Fernández Mir, Paul B. Jackson, Siddharth Bhat, Andrés Goens, Tobias Grosser. #ITP #Lean4 #Math
• Yet another formal theory of probabilities (with an application to random sampling). ~ Reynald Affeldt et als. #ITP #Coq #Math
• A zoo of continuity properties in constructive type theory. ~ Martin Baillon et als. #ITP #Coq
• PutnamBench: A multilingual competition-mathematics benchmark for formal theorem-proving. ~ George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, Swarat Chaudhuri. #ITP #Coq #IsabelleHOL #Lean4
• OnlineProver: A proof assistant for online teaching of formal logic and semantics. ~ Joachim Tilsted Kristensen et als. #Logic

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

• Lecturas compartidas el 17 de junio de 2024. #ITP #IsabelleHOL #FunctionalProgramming #Algorithms #AI
• Formally certified approximate model counting. ~ Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel. #ITP #IsabelleHOL
• Enriched category basics (in Isabelle/HOL). ~ Eugene W. Stark. #ITP #IsabelleHOL #Math
• Residuated transition systems II: Categorical properties (in Isabelle/HOL). ~ Eugene W. Stark. #ITP #IsabelleHOL
• Automated mathematical discovery and verification: Minimizing pentagons in the plane. ~ Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins. #ATP #SAT #Math
• Dive deeper into Prolog: Master the fundamentals and tackle complex AI challenges. ~ Ashani Sansala Kodithuwakku. #LogicProgramming #Prolog #AI
• Is programming by example solved by LLMs? ~ Wen-Ding L, Kevin Ellis. #LLMs #Programming
• Can AI models solve the programming challenge Advent of Code? (Evaluating state of the art large language models). ~ Johannes Sandström. #AI #LLMs #Programming
• GitHub Copilot: the perfect Code compLeeter? ~ Ilja Siroš, Dave Singelée, Bart Preneel. #AI #LLMs #Programming

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

• Lecturas compartidas el 16 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #CompSci #LambdaCalculus
• Functional data structures and algorithms (A proof assistant approach). ~ Tobias Nipkow (ed.). #ITP #IsabelleHOL #FunctionalProgramming #Algorithms
• Alpha-beta pruning (in Isabelle/HOL). ~ Tobias Nipkow. #ITP #IsabelleHOL #FunctionalProgramming #Algorithms
• This simple logic question stumps even the most advanced AI. ~ Maggie Harrison Dupré. #AI

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

• Lecturas compartidas el 15 de junio de 2024. #ITP #Lean4 #Rocq_Prover #Autoformalization #LLMs #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (15-junio-24). #ITP #Lean4 #IsabelleHOL #Math
• Libro "Calculemus (Demostraciones con Lean4)" (versión 16-junio-24). #ITP #Lean4 #Math
• Propositional calculus in Coq. ~ Floris van Doorn. #ITP #Coq #Logic #Math
• Foundations of programming languages. ~ Paul Downen. #CompSci
• Quantifier elimination — dense linear orders. ~ Joel David Hamkins. #Math
• Programming with math | The lambda calculus. ~ Eyesomorphic. #LambdaCalculus

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