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

• Lecturas compartidas el 28 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #LogicProgramming #Prolog
• #Exercitium: Reconocimiento de potencias de 2. #Haskell #Python #Matemáticas
• Logic and mechanized reasoning. ~ Jeremy Avigad, Marijn J. H. Heule, and Wojciech Nawrocki. #Logic #ITP #Lean4
• A formalization of the general theory of quaternions. ~Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón. #ITP #PVS #Math
• End-to-end formal verification of a fast and accurate floating-point approximation. ~ Florian Faissole, Paul Geneau de Lamarlière and Guillaume Melquiond. #ITP #Coq
• Formalising a number theory textbook: Lessons learnt. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math

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

• Lecturas compartidas el 27 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones convergentes son sucesiones de Cauchy". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Particiones de enteros positivos. #Haskell #Python #Matemáticas
• A "calculation-heavy" introduction to proof, with support from Lean. ~ Heather Macbeth. #ITP #Lean4
• Mastering QuickCheck: Advanced yet practical techniques for property-based testing. ~ Koz Ross. #FunctionalProgramming #Haskell
• Introducción a la programación lógica con Scryer Prolog. ~ Adrián Arroyo Calle. #LogicProgramming #Prolog

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

• Lecturas compartidas el 26 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂". #ITP #Lean4 #IsabelleHOL #Math
• Error bounds for floating points in Isabelle/HOL. ~ Jan Douwe Beekman. #ITP #IsabelleHOL
• Condensed mathematics in Mathlib. ~ Dagur Asgeirsson. #ITP #Lean4 #Math
• Tactics & keyframes: Visualizing Lean 4 proofs in Blender. ~ David Renshaw. #ITP #Lean4
• miniCodeProps: A minimal benchmark for proving code properties. ~ Evan Lohn, Sean Welleck. #ITP #Lean4 #LLMs
• FVEL: Interactive formal verification environment with large language models via theorem proving. ~ Xiaohan Lin et als. #ITP #IsabelleHOL #LLMs
• Proving olympiad algebraic inequalities without human demonstrations. ~ Chenrui Wei, Mengzhou Sun, Wei Wang. #AIPS #AI #ITP #Math

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

• Lecturas compartidas el 25 de junio de 2024. #ITP #Agda #Coq #HOL #HOL_Light #IsabelleHOL #Lean4 #Metamath #Math #Haskell #Python #Algorithms #AI #MachineLearning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La igualdad de valores es una relación de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• Products with unordered n-tuples. ~ Brent Yorgey. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 24 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La equipotencia es una relación de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Mínimo producto escalar. #Haskell #Python #Matemáticas
• Teaching mathematics to computers. ~ Kevin Buzzard. #ITP #Lean4 #Math #AI #MachineLearning
• Towards a formalized proof of Carleson's theorem. ~ Floris van Doorn. #ITP #Lean4 #Math
• Linear algebra game in Lean. ~ Sina Hazratpour. #ITP #Lean4 #Math
• Building measure theory using hierarchy builder. ~ Cyril Cohen. #ITP #Coq #Math
• Symbolic computation for all the fun. ~ Chad E. Brown, Mikoláš Janota, Mirek Olšák. #Math #ATP
• System introductions I: HOL (1). ~ Freek Wiedijk. #ITP #HOL
• More on HOL Light (2). ~ Freek Wiedijk. #ITP #HOL_Light
• Even more on HOL Light (3). ~ Freek Wiedijk. #ITP #HOL_Light
• Modularity in PVS. ~ Sam Owre. #ITP #PVS
• Lessons from Metamath. ~ Mario Carneiro. #ITP #Metamath
• A quick tour of Agda. ~ Guillaume Allais. #ITP #Agda
• Theorem proving and AI. ~ Josef Urban. #ATP #ITP #AI #Math
• System introductions I: Lean. ~ Mario Carneiro. #ITP #Lean4
• System introductions II: Isabelle. ~ Manuel Eberl. #ITP #IsabelleHOL
• System introductions: PVS. ~ Sam Owre. #ITP #PVS
• Reconciling type theory with the use of a single type of numbers for mathematical education at introductory levels. ~ Yves Bertot. #ITP #Coq #Math
• Programming mathematics: Tools and challenges. ~ Georges Gonthier. #ITP #Coq
• From informal to formal and back. ~ Patrick Massot. #ITP #Lean4 #Math
• Beautiful formalizations and proofs. ~ Natarajan Shankar. #ITP #PVS #Math
• Workshop: Formalization of Mathematics (June 2024). Hausdorff Center for Mathematics. #ITP #Math
• AI tools for Better Math. ~ Valeria de Paiva. #Math #AI
• La grande épopée des algorithmes. ~ Claire Mathieu. #Algorithms

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

• Lecturas compartidas el 23 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La equipotencia es una relación transitiva". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Números con dígitos primos. #Haskell #Python #Matemáticas
• Formalising advanced mathematics in Isabelle/HOL. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math

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

• Lecturas compartidas el 22 de junio de 2024. #ITP #IsabelleHOL #Lean4 #LLMs #Math #Reasoning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La composición de funciones biyectivas es biyectiva". #ITP #Lean4 #IsabelleHOL #Math
• Libro "Calculemus (Demostraciones con Lean4)" (versión 23-junio-24). #ITP #Lean4 #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (23-junio-24). #ITP #Lean4 #IsabelleHOL #Math
• Competitive programming in Haskell: sieving with mutable arrays. ~ Brent Yorgey. #FunctionalProgramming #Haskell

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

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. #Algorithms #FunctionalProgramming #ITP #Deduce
• Deduce: A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs. ~ Jeremy Siek. #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, Andres Löh. #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. #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

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

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

• Lecturas compartidas el 26 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones convergentes están acotadas". #ITP #Lean4 #IsabelleHOL #Math
• Autoformalizing euclidean geometry. ~ Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si. #Autoformalisation #LLMs #ITP #Lean4
• Coding in Haskell: Writing and debugging megaparsec parsers for grep. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 26 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Go #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Un número es par si y solo si lo es su cuadrado". #ITP #Lean4 #IsabelleHOL #Math
• Proofs for a price: Tomorrow’s ultra-rigorous mathematical culture. ~ Silvia De Toffoli. #Math #ITP
• Poincaré on the value of reasoning machines. ~ Colin McLarty. #Math #ITP
• AlephZero and mathematical experience. ~ Simon DeDeo. #Math #AI #ITP
• Working with machines in mathematics. ~ Alex Davies. #Math #MachineLearning
• Automated mathematics and the reconfiguration of proof and labor. ~ Rodrigo Ochigame. #Math #ITP
• Machine Learning and Information Theory Concepts towards an AI Mathematician. ~ Yoshua Bengio and Nikolay Malkin. #Math #AI #ITP
• How to calculate pi in a new way. ~ Mahdi Sasar. #Math

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

• Lecturas compartidas el 25 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #LLMs #MachineLearning
• Libro "Calculemus (Demostraciones con Lean4)" (versión 25-mayo-24). #ITP #Lean4 #Math
• Generating executable Go code from the Isabelle theorem prover. ~ Matthias Stübinger. #ITP #IsabelleHOL #Go

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

• Lecturas compartidas el 24 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math
• #Exercitium: Conjunto de primos relativos. #Haskell #Python #Matemáticas
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (25-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Statically typed functional programming with Python 3.12. ~ Oskar Wickström. #FunctionalProgramming #Python
• Proving theorems recursively. ~ Haiming Wang et als. #ITP #IsabelleHOL #LLMs #MachineLearning
• DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. ~ Huajian Xin et als. #LLMs #ITP #Lean4

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

• Lecturas compartidas el 23 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Math #AI
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Los supremos de las sucesiones crecientes son sus límites". #ITP #Lean4 #IsabelleHOL #Math
• Towards mechanised consensus in Isabelle. ~ Elliot Jones and Diego Marmsoler. #ITP #IsabelleHOL
• Towards formally specifying and verifying smart contract upgrades in Coq. ~ Derek Sorensen. #ITP #Coq

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

• Lecturas compartidas el 22 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva". #ITP #Lean4 #IsabelleHOL #Math
• VOLPIC: Verifying lifted Pascal in Coq. ~ Charles Averill. #ITP #Coq
• The Haskell Unfolder Episode 26: Variable-arity functions. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Why mathematics is set to be revolutionized by AI. ~ Thomas Fink. #Math #AI
• Online historical maths textbooks. #Math

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

• Lecturas compartidas el 21 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #SMT #Z3 #FunctionalProgramming #Haskell #Python #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si una función es creciente e involutiva, entonces es la identidad". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 20 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La composición de una función creciente y una decreciente es decreciente". #ITP #Lean4 #IsabelleHOL #Math
• On the ingredients for Fermat. ~ Kevin Buzzard. #ITP #Lean4 #Math
• Quiver: Guided abductive inference of separation logic specifications in Coq. ~ Simon Spies, Lennard Gäher, Michael Sammler and Derek Dreyer. #ITP #Coq
• Proving Sum n = n*(n-1)/2 and that 1/n tends to 0. ~ Philip Zucker. #Python #SMT #Z3
• Prefer do notation over Applicative operators when assembling records. ~ Gabriella Gonzalez #FunctionalProgramming #Haskell
• Beauty is not simplicity: An analysis of mathematicians' proof appraisals. ~ Matthew Inglis and Andrew Aberdein. #Math

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

• Lecturas compartidas el 19 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Haskell #Python #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Los monoides booleanos son conmutativos". #ITP #Lean4 #IsabelleHOL #Math
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Linear resources in Isabelle/HOL. ~ Filip Smola and Jacques D. Fleuriot. #ITP #IsabelleHOL
• Grothendieck's use of equality. ~ Kevin Buzzard. #Math #ITP #LeanProver
• Beyond trees: Calculating graph-based compilers. ~ Patrick Bahr and Graham Hutton. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 18 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Agda #Physics #Math #Programming #Python
• Libro "Calculemus (Demostraciones con Lean4)" (versión 18-mayo-24). #ITP #Lean4 #Math
• #Exercitium: Diferencia simétrica. #Haskell #Python #Matemáticas
• Bridging syntax and semantics of Lean expressions in E-Graphs. ~ Marcus Rossel and Andrés Goens. #ITP #Lean4
• PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL. ~ Andreas Viktor Hess, Sebastian Alexander Mödersheim, Achim D. Brucker and Anders Schlichtkrull. #ITP #IsabelleHOL
• Metamathematics. ~ David Marker. #Logic #Math

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

• Lecturas compartidas el 17 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (18-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Proofs and conversations. ~ Talia Ringer. #ITP #Coq #Math
• Functional induction. ~ Joachim Breitner. #ITP #Lean4
• HepLean: Digitalising high energy physics. ~ Joseph Tooby-Smith. #ITP #Lean4 #Physics
• Foundational verification of smart contracts through verified compilation. ~ Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao. #ITP #Coq
• Initial algebras unchained (A novel initial algebra construction formalized in Agda). ~ Thorsten Wißmann and Stefan Milius. #ITP #Agda #Math
• Programming as a mediator of mathematical thinking (Examples from upper secondary students exploring the definite integral). ~ Timo Tossavainen, Claes Johansson, Alf Juhlin and Anna Wedestig. #Math #Programming #Python
• Math databases. ~ Jeremy Kun. #Math
• code4math: Consortium of digital ecosystems for mathematics. #Math

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

• Lecturas compartidas el 16 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Logic #Math #FunctionalProgramming #Haskell #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)ⁿ". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 15 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #PVS #Coq #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c". #ITP #Lean4 #IsabelleHOL #Math
• Course: Logic in Software Engineering (Lean). ~ Alexander Kurz. #ITP #Lean4 #Logic
• Interactive theorem proving:Introduction to Agda. ~ Jeremy Siek. #ITP #Agda
• Implementing categorical notions of partiality and delay in Agda. ~ Leon Vatthauee. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating Large Language Model performance on Haskell. ~ Andrew Chen. #LLMs #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 25: from Java to Haskell. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

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

• Lecturas compartidas el 14 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Haskell #Python #Math #Emacs #OrgMode #Elisp #ChatGPT
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a". #ITP #Lean4 #IsabelleHOL #Math
• Towards nominal AC-unification. ~ Gabriel Ferreira Silva. #PhDThesis #ITP #PVS
• Multris: Functional verification of multiparty message passing in separation logic. ~ Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers. #ITP #Coq

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

• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Matrices de Toepliz. #Haskell #Python #Matemáticas
• Schönhage-Strassen multiplication (in Isabelle/HOL). ~ Jakob Schulz. #ITP #IsabelleHOL #Math
• An entry into the world of Org Mode for non Emacs users. ~ James Stoup. #Emacs #OrgMode
• Writing Lisp code with ChatGPT. #Elisp #ChatGPT

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

• Lecturas compartidas el 12 de mayo de 2024. #ITP #Lean4 #Agda #Math #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G un grupo y a, b ∈ G tales que a⋅b = 1, entonces a⁻¹ = b". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 11 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
• Libro "Calculemus (Demostraciones con Lean4)" (versión 11-mayo-24). #ITP #LeanProver #Lean4 #Matemáticas
• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #Lean4 #Math
• Agda core: The dream and the reality. ~ Jesper Cockx #ITP #Agda
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 10 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #SAT_solver #FunctionalProgramming #Haskell #Python #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (11-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math
• Course: Formalising Mathematics in Lean. ~ Adrián Doña Mateo, Monica Abu Omar, Patrick Kinnear and Simone Castellan. #ITP #Lean4 #Math
• Course: Formalized Mathematics in Lean (Winter 23/24). ~ Floris van Doorn. #ITP #Lean4 #Math
• Course: Theorem proving with Lean. ~ Damiano Testa. #ITP #Lean4 #Math
• Partial correctness of the top-down solver (in Isabelle/HOL). ~ Yannick Stade, Sarah Tilscher, Helmut Seidl. #ITP #IsabelleHOL
• LL(1) parser generator (in Isabelle/HOL). ~ Sarah Tilscher and Simon Wimmer. #ITP #IsabelleHOL
• How to explore Lisp metaprogramming techniques. #CommonLisp
• The way of Lisp or the right way. ~ Joe Marshall. #Lisp #Programming

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

• Lecturas compartidas el 9 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #CategoryTheory
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de la unicidad del elemento neutro en los grupos. #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Diagonales principales de una matriz. #Haskell #Python #Matemáticas
• Verifying a SAT solver from ground up. ~ Mathias Fleury. #ITP #IsabelleHOL #SAT_solver
• Solving recurrence relations. ~ John Mount. #Python #Math

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

• Lecturas compartidas el 8 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces a⋅b = a ↔ b = 1". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #Matemáticas
• Compiling higher order functions with GADTs. ~ Srijan. #FunctionalProgramming #Haskell
• When are functions lazy enough for lists. ~ Daniel Beskin. #FunctionalProgramming #Haskell
• Notes on Category Theory (with examples from basic mathematics). ~ Paolo Perrone. #CategoryTheory

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

• Lecturas compartidas el 7 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #SMT #Logic #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide conmutativo y x, y, z ∈ M tales que x⋅y = 1 y x⋅z = 1, entonces y = z.". #ITP #Lean4 #IsabelleHOL #Math
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• HOL4P4: Mechanized small-step semantics for P4. ~ Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam. #ITP #HOL4

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

• Lecturas compartidas el 6 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #AI #LLMs #Programming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Sea M un monoide y a, b ∈ M tales que ab = 1. Entonces, a = 1 si y sólo si b = 1". #ITP #Lean4 #IsabelleHOL #Math
• Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. #ITP #Agda #Math
• NL2FOL: Translating natural language to first-order logic for logical fallacy detection. ~ Abhinav Lalwani, Lovish Chopra, Christopher Hahn, Caroline Trippel, Zhijing Jin, Mrinmaya Sachan. #LLMs #SMT #Logic

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

• Lecturas compartidas el 5 de mayo de 2024. #ITP #IsabelleHOL #Lean4 #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide, x ∈ M y m, n ∈ N, entonces x^(m+n)=x^m · x^n". #ITP #Lean4 #IsabelleHOL #Math
• Formalizing Pick's theorem in Isabelle/HOL. ~ Sage Binder, Katherine Kosaian. #ITP #IsabelleHOL #Math
• Guided equality saturation. ~ Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer. #ITP #Lean4
• An introduction to MathComp-Analysis. ~ Reynald Affeldt. #ITP #Coq #Math
• Formalizing soundness proofs of linear PCP SNARKs. ~ Bolton Bailey, Andrew Miller. #ITP #Lean4
• Automatic programming: Large language models and beyond. ~ Michael R. Lyu, Baishakhi Ray, Abhik Roychoudhury, Shin Hwei Tan, Patanamon Thongtanunam. #LLMs #Programming

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

• Lecturas compartidas el 4 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #AI
• Libro "Calculemus (Demostraciones con Lean4)" (versión 4-mayo-24). #ITP #LeanProver #Lean4 #Matemáticas
• Verification and refinement of natural language explanations through LLM-symbolic theorem proving. ~ Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas. #AI #LLMs #ITP #IsabelleHOL

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

• Lecturas compartidas el 3 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #CompSci #Education #AI #GenerativeAI #MachineLearning #DeepLearning
• Libro "Piensa en Haskell y en Python" (versión del 3-may-24). #Haskell #Python #Matemáticas #Algorítmica
• Resumen de lecturas compartidas durante abril de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (4-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Substitutions for lambda-free higher-order terms (in Isabelle/HOL). ~ Vincent Trélat. #ITP #IsabelleHOL
• A narrative history of Artificial Intelligence. ~ Masayuki Ida. #AI