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

• Lecturas compartidas el 21 de junio de 2024. #ITP #Coq #FunctionalProgramming #OCaml
• Carleson operators on doubling metric measure spaces, ~ Lars Becker, Floris van Doorn, Asgar Jamneshan, Rajula Srivastava, Christoph Thiele. #ITP #Lean4 #Math
• Lean4trace: Data augmentation for neural theorem proving in Lean. ~ Vasilii Nesterov, Yermek Kapushev, Mikhail Burtsev. #ITP #Lean4 #LLMs
• More details, please: Improving autoformalization with more detailed proofs. ~ Guillem Tarrach, Albert Q. Jiang, Daniel Raggi, Wenda Li, Mateja Jamnik. #ITP #IsabelleHOL #LLMs
• VerityMath: Advancing mathematical reasoning by self-verification through unit consistency. ~ Vernon Toh Yan Han, Ratish Puduppully, Nancy F. Chen. #LLMs #Math #Reasoning

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

• Lecturas compartidas el 20 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math
• Verified extraction from Coq to OCaml. ~ Yannick Forster, Matthieu Sozeau, Nicolas Tabareau. #ITP #Coq #FunctionalProgramming #OCaml
• A verified compiler for a functional tensor language. ~ Amanda Liu,Gilbert Bernstein,Adam Chlipala,Jonathan Ragan-Kelley. #ITP #Coq
• Live verification in an interactive proof assistant. ~ Samuel Gruetter,Viktor Fukala,Adam Chlipala. #ITP #Coq

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. #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. #Math