The readings shared in Mastodon on August 15, 2024 are

• Readings shared August 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• Software verification with Isabelle/HOL. ~ Peter Höfner. #ITP #IsabelleHOL
• Functional algorithms verified in SSReflect. ~ Alex Gryzlov et als. #ITP #Coq #SSReflect
• Haskell for Elm developers: giving names to stuff (Part 5 - Semigroups and Monoids). ~ Flavio Corpa. #Haskell #Elm #FunctionalProgramming
• The Haskell Unfolder Episode 31: nothunks. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Galois theory. ~ Tom Leinster. #Math

The readings shared in Mastodon on August 14, 2024 are

• Readings shared August 13, 2024. #ITP #Coq #Agda #Math #Python
• #Calculemus: Proofs with Lean4 and Isabelle/HOL of "take n xs ++ drop n xs = xs". #ITP #Lean4 #IsabelleHOL #Math
• Introduction to proofs with Lean proof assistant. ~ Sina Hazratpour. #ITP #LeanProver
• Taller de Lean 4. ~ Enric Cosme, Mario Vago. #ITP #LeanProver #Lean4
• A topological approach for semi-supervised learning. ~ Adrián Inés, César Domínguez, Jónathan Heras, Gadea Mata & Julio Rubio. #AI #MachineLearning #Math

The readings shared in Mastodon on August 13, 2024 are

• Readings Shared August 13, 2024. #Python #Haskell #FunctionalProgramming
• An elementary proof of the FMP for Kleene algebra. ~ Tobias Kappé. #ITP #Coq #Math
• Sharing proofs with predicative theories through universe-polymorphic elaboration. ~ Thiago Felicissimo & Frédéric Blanqui. #ITP #Agda #Coq
• Bounding Euler's constant. ~ Philip Zucker. #Math #Python
• Algebra. It's powerful. But it's not what it was. ~ Keith Devlin. #Math

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

• Lecturas compartidas el 9 de agosto de 2024. #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA
• Function composition and currying in Python (Python in the streets, Haskell in the sheets!). ~ Francisco Gutierrez. #Python #Haskell #FunctionalProgramming

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

• Lecturas compartidas el 8 de agosto de 2024. #ITP #Lean4 #IsabelleHOL #Math #DeepLearning
• A tricky lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Verified transformations for convex programming. ~ Ramon Fernández Mir. #ITP #Lean4 #Math
• First steps towards computational polynomials in Lean. ~ James Harold Davenport. #ITP #LeanProver #Math
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner & Detlef Plump. #ITP #IsabelleHOL
• Validation of a formal floating-point model for the interactive proof assistant Isabelle/HOL. ~ Olof Lindström. #ITP #IsabelleHOL
• Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. #ITP #HOL4
• An in-context learning agent for formal theorem-proving. ~ Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri. #LLMs #ITP #Coq #LeanProver
• Competitive programming in Haskell: Tree path decomposition, part II. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• typedKanren: Statically typed relational programming with exhaustive matching in Haskell. ~ Nikolai Kudasov & Artem Starikov. #Haskell #FunctionalProgramming
• Combinatorial and algorithmic mathematics (From foundation to optimization) ~ Baha M. Alzalg #Math
• Intelligent Computer Mathematics (17th International Conference, CICM 2024, Proceedings) #ITP #Math
• The potential for AI in science and mathematics. ~ Terence Tao. #IA #Math #ITP #LeanProver

Las lecturas compartidas en Mastodon el 08 de agosto de 2024 son

• Lecturas compartidas el 6 de agosto de 2024. #ITP #Coq #Python #FunctionalProgramming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length(xs ++ ys) = length(xs) + length(ys)". #ITP #Lean4 #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si. #ITP #DeepLearning
• Getting started with Blueprint-Driven formalization projects in Lean. ~ Pietro Monticone. #ITP #LeanProver #Lean4

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

• Lecturas compartidas el 5 de agosto de 2024. #ATP #SAT #Haskell #FunctionalProgramming #CurryHoward #TypeScript
• Rely-guarantee semantics for separation-logic-based specification extraction. ~ Paul He. #PhDThesis #ITP #Coq
• Functional programming in Python: When and how to use it. ~ John Sturtz. #Python #FunctionalProgramming

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

• Lecturas compartidas el 4 de agosto de 2024. #ITP #IsabelleHOL #Diproche #Math
• A SAT-based approach to rigorous verification of Bayesian networks. ~ Ignacy Stępka, Nicholas Gisolfi & Artur Dubrawski. #ATP #SAT
• Why does everyone hate Haskell, jazz, and pure math? ~ Adam Dueck. #Haskell #FunctionalProgramming
• Proofs are programs: A few examples of the Curry-Howard correspondence. ~ Adam Dueck. #CurryHoward #TypeScript

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

• Lecturas compartidas el 3 de agosto de 2024. #Math
• The top-down solver verified: Building confidence in static analyzers. Yannick Stade, Sarah Tilscher & Helmut Seidl. #ITP #IsabelleHOL
• Sociomathematical norms and automated proof checking in mathematical education: Reflections and experiences. ~ Merlin Carl. #ITP #Diproche #Math

Las lecturas compartidas en Mastodon el 3 de agosto de 2024 son

• Lecturas compartidas el 2 de agosto de 2024. #ITP #LeanProver #IsabelleHOL #Coq #MinLog #Agda #Logic #Math #FunctionalProgramming #Haskell #Hope #Miranda
• A guide to writing mathematics. ~ Kevin P. Lee. #Math
• How to write mathematics. ~ Paul R. Halmos. #Math

Las lecturas compartidas en Mastodon el 2 de agosto de 2024 son

• Lecturas compartidas el 1 de agosto de 2024. #ITP #Lean4 #Mathlib #Coq #Math #Haskell #FunctionalProgramming
• Semialgebraic groups and generalized affine buildings. ~ Raphael Appenzeller. #PhDThesis #ITP #LeanProver #Math
• Lie groups and algebras (in Isabelle/HOL). ~ Richard Schmoetten & Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• Semantical analysis of intuitionistic modal logics between CK and IK. ~ Jim de Groot, Ian Shillito & Ranald Clouston. #ITP #Coq #Logic
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis. ~ Grigory Devadze, Victor Magron & Stefan Streif. #ITP #MinLog #Math
• A framework for semiring-annotated type systems. ~ James Wood. #ITP #Agda #TypeTheory
• Where does the name "algebraic data type" come from? ~ Li-yao Xia. #FunctionalProgramming #Hope #Miranda
• Analyzing Haskell stability. ~ Jappie Klooster. #Haskell #FunctionalProgramming
• Data.Maybe, and thoughts on library design. ~ Srijan Paul. #Haskell #FunctionalProgramming
• Esta vez sí: Con la IA, nada será igual en la Universidad. ~ Mariano Fernández Enguita. #IA #Educación
• La demanda de educación superior ante el cambio tecnológico y la inteligencia artificial. ~ José Ignacio Conde-Ruiz, Juan José Ganuza, Manu García y Carlos Victoria. #IA #Educación
• Inteligencia Artificial y capital humano: ¿Pueden estar en peligro sus complementariedades? ~ Juan F. Jimeno y Ana Lamo. #IA

Las lecturas compartidas en Mastodon el 1 de agosto de 2024 son

• Lecturas compartidas el 31 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #LLMs #ATP #Reasoning
• Continuous functions — formalized in Lean4. ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• Continuous functions — formalized in Lean4 (code and a LaTeX document). ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• LeanSearch: Find theorems in Mathlib4 using natural language query. #ITP #Lean4 #Mathlib
• Search Mathlib: A webpage that searches for Mathlib theorems. ~ Deming Xu. #ITP #Lean4 #Mathlib
• Set Theory Game (An introduction to mathematical proof). ~ Daniel J. Velleman./#/g/djvelleman/stg4 #ITP #Lean4 #Math
• Lean Game Server (A repository of learning games for the proof assistant Lean (Lean 4) and its mathematical library Mathlib). #ITP #Lean4 #Math
• A verified foreign function interface between Coq and C. ~ Joomy Korkut, Kathrin Stark, Andrew W. Appel. #ITP #Coq
• The Haskell Unfolder Episode 30: runST. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 31 de julio de 2024 son

• Lecturas compartidas el 30 de julio de 2024. #ITP #IsabelleHOL #Math #LogicProgramming #ASP #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Asociatividad de la concatenación de listas". #ITP #Lean4 #IsabelleHOL #Math
• A formalization and proof checker for Isabelle’s metalogic. ~ Simon Roßkopf, Tobias Nipkow. #ITP #IsabelleHOL
• From Schütte’s formal systems to modern automated deduction. ~ Wolfgang Bibel, Jens Otten. #ATP #Logic
• Steamroller problems: An evaluation of LLM reasoning capability with automated theorem prover strategies. ~ Lachlan McGinness, Peter Baumgartner. #LLMs #ATP #Reasoning

Las lecturas compartidas en Mastodon el 30 de julio de 2024 son

• Lecturas compartidas el 29 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #AI #CAS
• A construction of the Lie algebra of a Lie group in Isabelle/HOL. ~ Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• LLASP: Fine-tuning Large Language Models for Answer Set Programming. ~ Erica Coppolillo, Francesco Calimeri, Giuseppe Manco, Simona Perri, Francesco Ricca. #AI #LLMs #LogicProgramming #ASP
• AlphaProof, AlphaGeometry, ChatGPT, and why the future of AI is neurosymbolic. ~ Gary Marcus. #AI
• CalcGPT, la calculadora inútil pero «inteligente». ~ @Alvy. #ChatGPT #Math

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

• Lecturas compartidas el 28 de julio de 2024. #ITP #LeanProver #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length (replicate n x) = n". #ITP #Lean4 #IsabelleHOL #Math
• Advancing mathematics through computers and AI: Automation, discovery, and collaboration. ~Douglas C. Youvan. #AI #ITP #CAS #Math

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

• Lecturas compartidas el 27 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Formalisation of the finite simple Conway groups in Lean. ~ Erik van der Plas. #ITP #LeanProver #Math
• The first Janko group J1: simplicity and formalization. ~ Roxy van de Kuilen. #ITP #LeanProver #Math

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

• Lecturas compartidas el 26 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #IMO #AI #AlphaProof #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n". #ITP #Lean4 #IsabelleHOL #Math
• Haskell nuggets: k-means. ~ Justin Lê. #FunctionalProgramming #Haskell
• Prove or disprove. 100 conjectures from the OEIS. ~ Ralf Stephan. #Math

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

• Lecturas compartidas el 25 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones divergentes positivas no tienen límites finitos". #ITP #Lean4 #IsabelleHOL #Math
• AI achieves silver-medal standard solving International Mathematical Olympiad problems. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Google DeepMind IMO 2024 Solutions. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Move over, mathematicians, here comes AlphaProof (A.I. is getting good at math — and might soon make a worthy collaborator for humans). ~ Siobhan Roberts. #AI #Math #IMO #Lean4 #AlphaProof
• To formalized mathematics and back with the Lean theorem prover. ~ Kyle Miller. #ITP #LeanProver #Math
• The mysteries and frustrations of numerical proofs. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Formal verification of 2-3 trees in Coq. ~ Horia-Matei Cornea. #ITP #Coq
• Rivers: eventually constant streams in Haskell. ~ Brent Yorgey. #FunctionalProgramming #Haskell
• Types as interfaces. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 24 de julio de 2024. #ITP #Lean4 #Coq #Logic #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u". #ITP #Lean4 #IsabelleHOL #Math
• Approximate relational reasoning for higher-order probabilistic programs. ~ Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal. #ITP #Coq
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover. ~ Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen. #LLMs #ITP #Lean4 #Math

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

• Lecturas compartidas el 23 de julio de 2024. #ITP #Lean4 #Math #FunctionalProgramming #OCaml
• Lean For Haskell developers. ~ Solomon. #ITP #Lean4 #FunctionalProgramming #Haskell
• A logic for veracity: Development and implementation. ~ Daniel Britten, Steve Reeves. #ITP #Coq #Logic
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue, Takafumi Saikawa. #ITP #Coq

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

• Lecturas compartidas el 22 de julio de 2024. #AI
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean. ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean (Code). ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• (Pro)Seminar on computer-assisted mathematics. ~ Judith Ludwig, Florent Schaffhauser. #CAS #Sage #ITP #LeanProver #Math
• Practical deductive verification of OCaml programs (Extended version). ~ Mário Pereira. #FunctionalProgramming #OCaml

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

• Lecturas compartidas el 21 de julio de 2024. #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell
• Un robot que resuelve rompecabezas 200 veces más rápido que las personas más hábiles. ~ @Alvy. #AI

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

• Lecturas compartidas el 20 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Logic #CompSci
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• A tree rewriting system for the Reflection Calculus. ~ Sofía Santiago-Fernández, Joost J. Joosten, David Fernández-Duque. #ITP #Coq #Logic
• Automated proof tactics for model transformation. ~ Julien Cohen, Massimo Tisi, Remi Douence. #ITP #Coq
• Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. #FunctionalProgramming #Haskell #LiquidHaskell
• Monumental proof settles geometric Langlands conjecture. ~ Erica Klarreich. #Math

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

• Lecturas compartidas el 19 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin, Zhiqing Sun, Yiming Yang, Sean Welleck. #ITP #Lean4 #LLMs
• PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition. ~ George Tsoukalas et als. #LLMs #ITP #Lean4 #IsabelleHOL #Coq
• Haskelite: A tracing interpreter based on a pattern-matching calculus. ~ Pedro Vasconcelos, Rodrigo Marques. #FunctionalProgramming #Haskell
• Higher-order specifications for deductive synthesis of programs with pointers. ~ David Young et als. #FunctionalProgramming #Pika
• The significance of symbolic logic for scientific education. ~ André Platzer. #Logic #CompSci

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

• Lecturas compartidas el 18 de julio de 2024. #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "El punto de acumulación de las sucesiones convergente es su límite". #ITP #Lean4 #IsabelleHOL #Math
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als. #ITP #Lean4 #Math
• Haskell for dilettantes, Part 1: Intro. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 2: Expressions, types, and functions. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 3a: Homework 1, Exercise 1. ~ Tea Leaves. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 16 de julio de 2024. #ITP #Lean4 #Coq #LLMs #Programming #Emacs
• Functional Pearl: Short and mechanized logical relation for dependent type theories. ~ Yiyun Liu, Stephanie Weirich. #ITP #Coq
• HHLPar: Automated theorem prover for parallel hybrid communicating sequential processes. ~ Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan. #ITP #IsabelleHOL
• Molly: A verified compiler for cryptographic roles. ~ Daniel J. Dougherty, Joshua D. Guttman. #ITP #Coq
• Formalizing operads for a categorical framework of DSL composition. ~ Zachary Flores, Angelo Taranto, Yakir Forman, Eric Bond. #ITP #Coq
• Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. #FunctionalProgramming #LiquidHaskell
• Demystifying Artificial Intelligence (Symbolic, data-driven, statistical and ethical AI). ~ Emmanuel Gillain (ed.). #eBook #AI
• Using ChatGPT as a proof assistant in a mathematics pathways course. ~ Hyejin Park, Eric D. Manley. #ChatGPT #Math #Reasoning
• The Haskell Unfolder Episode 29: Exceptions, annotations and backtraces. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

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

• Lecturas compartidas el 15 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #CompSci #Haskell #Prolog
• A term-patching framework for eliminating definitional equalities in Lean (Work-in-progress). ~ Rishikesh Vaishnav. #ITP #Lean4
• Guided proof search using large language models and lemma extraction in Coq. ~ Tarun Prasad. #ITP #Coq #LLMs
• Code completion with Google Gemini for Emacsen. ~ Hitoshi Uchida. #Programming #Emacs #Gemini

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

• Lecturas compartidas el 14 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Haskell #Prolog
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las subsucesiones tienen el mismo límite que la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• Formalizing implicational axiomatics for classical first-order logic with functions in Isabelle/HOL. ~ Jørgen Villadsen, Roberto Pettinau. #ITP #IsabelleHOL #Logic
• Mathematics in programming. ~ Xinyu Liu #Math #CompSci #Haskell
• Smart investment problem with Prolog. ~ Matteo Redaelli. #Prolog

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

• Lecturas compartidas el 13 de julio de 2024. #ITP #Lean4 #Coq #Abella #Agda #Mizar #Logic #Math #IMO #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]". #ITP #Lean4 #IsabelleHOL #Math
• Implementing the Fatio protocol for multi-agent argumentation in LogiKEy. ~ Luca Pasetto, Christoph Benzmüller. #Logic #ITP #IsabelleHOL
• Implementing intermediate logics. ~ Bastiaan Haaksema, Jens Otten, Revantha Ramanayake. #ATP #Logic #Haskell #Prolog

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

• Lecturas compartidas el 12 de julio de 2024. #ITP #Coq #Logic #Math #FunctionalProgramming #Haskell #Physics
• IMO 1987 Problem 4: Animated Lean 4 proof. ~ David Renshaw. #ITP #Lean4 #Math #IMO
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu. #ITP #Coq #Logic #Math
• Binding contexts as partitionable multisets in Abella. ~ Terrance Gray, Gopalan Nadathur. #ITP #Abella
• Domain theory in univalent foundations I: Directed complete posets and Scott's D∞. ~ Tom de Jong. #ITP #Agda
• Domain theory in univalent foundations II: Continuous and algebraic domains. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda
• Separable polynomials and separable extensions. ~ Christoph Schwarzweller. #ITP #Mizar #Math
• Integral of continuous three variable functions. ~ Noboru Endou. #ITP #Mizar #Math
• Competitive programming in Haskell: Tree path decomposition, part I. ~ Brent Yorgey. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 11 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• Functional programming in learning electromagnetic theory. ~ Scott N. Walck. #FunctionalProgramming #Haskell #Physics
• Building a data compression utility in Haskell using Huffman codes. ~ Marcelo Lazaroni. #FunctionalProgramming #Haskell
• Collatz computations in base 2 and 3. ~ Chris Smith. #FunctionalProgramming #Haskell #Math
• The flower calculus. ~ Pablo Donato. #ITP #Coq #Logic

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

• Lecturas compartidas el 10 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Abella #Beluga #Agda #Haskell #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones de extracción no están acotadas". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 9 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Relación entre los índices de las subsucesiones y de la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• On non-triviality of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu. #ITP #Coq
• Binding contexts as partitionable multisets in Abella. ~ Terrance Gray, Gopalan Nadathur. #ITP #Abella
• A Beluga formalization of the Harmony Lemma in the π-calculus. ~ Gabriele Cecilia, Alberto Momigliano. #ITP #Beluga
• Confluence by the Z-property for De Bruijn’s λ-calculus with nameless dummies, based on PLFA∗. ~ Vincent van Oostrom. #ITP #Agda
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, Tobias Grosser. #ITP #Lean4
• Moca 0.3: A first-order theorem prover for Horn clauses. ~ Yusuke Oi, Nao Hirokawa, Teppei Saito. #Haskell #ATP #Logic

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

• Lecturas compartidas el 8 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• Lean: First steps (05 - Inequalities). ~ Tariq Rashid. #ITP #Lean4 #Math
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #Lean4
• Normative conditional reasoning as a fragment of HOL. ~ Xavier Parent, Christoph Benzmüller. #ITP #IsabelleHOL #Logic

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

• Lecturas compartidas el 7 de julio de 2024. #ITP #IsabelleHOL #Lean4 #Coq #Agda #Math #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones transitivas". #ITP #Lean4 #IsabelleHOL #Math
• Mechanised uniform interpolation for modal logics K, GL, and iSL. ~ Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito. #ITP #Coq #Logic

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

• Lecturas compartidas el 6 de julio de 2024. #ITP #Coq #Math
• Lean: Past, present, and future. ~ Sebastian Ullrich. #ITP #Lean4
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als. #ITP #Lean4 #Math
• A Lean formalization of Cedar. ~ Bhakti Shah. #ITP #Lean4
• A verified algorithm for deciding pattern completeness. ~ René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL #Haskell
• On synthesising Linux kernel module components from Coq formalisations. ~ Mario Frank. #PhDThesis #ITP #Coq
• Monads, comonads, and transducers. ~ Rafał Stefański. #ITP #Coq
• Machine-checked categorical diagrammatic reasoning. ~ Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez. #ITP #Coq
• Mechanized subject expansion in uniform intersection types for perpetual reductions. ~ Andrej Dudenhefner, Daniele Pautasso. #ITP #Coq
• Substitution for non-wellfounded syntax with binders through monoidal categories. ~ Ralph Matthes, Kobe Wullaert, Benedikt Ahrens. #ITP #Coq
• Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Émile Oleon. #ITP #Agda #Math

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

• Lecturas compartidas el 5 de julio de 2024. #ATP #ITP #IsabelleHOL #Lean4 #Logic #Math #FunctionalProgramming #Haskell #OCaml
• With fifth busy beaver, researchers approach computation’s limits (After decades of uncertainty, a motley team of programmers has proved precisely how complicated simple computer programs can get). ~ Ben Brubaker. #ITP #Coq #Math

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

• Lecturas compartidas el 4 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las familias de conjuntos definen relaciones simétricas". #ITP #Lean4 #IsabelleHOL #Math
• Automated reasoning for mathematics. ~ Jeremy Avigad. #ATP #ITP #Math
• Fast and verified UNSAT certificate checking. ~ Peter Lammich. #ITP #IsabelleHOL #SAT
• Formalizing chemical physics using the Lean theorem prover. ~ Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, Tyler R. Josephson. #ITP #Lean4
• Formalising Fermat’s last theorem for exponent 3 in Lean. ~ Pietro Monticone. #ITP #Lean4 #Math
• Verificació formal de formes equivalents de l’axioma d’elecció. ~ Vicent Pons Llopis. #TFG #ITP #Lean4 #Math
• An empirical assessment of progress in automated theorem proving. ~ Geoff Sutcliffe et als. #ATP
• Lemma discovery and strategies for automated induction. ~ Sólrún Halla Einarsdóttir, Márton Hajdu, Moa Johansson, Nicholas Smallbone, Martin Suda. #FunctionalProgramming #Haskell
• A technological approach to teaching inequalities, propositional and predicate logic. ~ Zoltán Kovács, Reinhard Oldenburg. #Logic #GeoGebra
• A natural-language proof assistant for higher-order logic (Work in progress). ~ Adam Dingle. #ITP #Natty #OCaml
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #OCaml
• Learning formal mathematics from intrinsic motivation. ~ Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman. #Math #AI
• The sad state of property-based testing libraries. ~ #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 3 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones reflexivas". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Número de divisores. #Haskell #Python #Matemáticas
• Lean: First steps. #ITP #Lean4 #Math
• TheoremLlama: Transforming general-purpose LLMs into Lean4 experts. ~ Ruida Wang et als. #ITP #Lean4 #LLMs
• The Haskell Unfolder Episode 28: Type families and overlapping instances. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 3 de julio de 2024 son

• Lecturas compartidas el 2 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #CategoryTheory #FunctionalProgramming #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las clases de equivalencia de elementos no relacionados son disjuntas". #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "El conjunto de las clases de equivalencia es una partición". #ITP #Lean4 #IsabelleHOL #Math

Las lecturas compartidas en Mastodon el 2 de julio de 2024 son

• Lecturas compartidas el 1 de julio de 2024. #ITP #IsabelleHOL #Lean4 #Math #AI #MachineLearning #DeepLearning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las clases de equivalencia de elementos relacionados son iguales". #ITP #Lean4 #IsabelleHOL #Math
• Extending Isabelle/HOL's code generator with support for the Go programming language. ~ Terru Stübinger, Lars Hupel. #ITP #IsabelleHOL
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt, Zachary Stone. #ITP #Coq #Math
• This month in Mathlib (May 2024). #ITP #Lean4 #Mathlib #Math
• Folding in parallel. ~ Oleg Kiselyov. #FunctionalProgramming #Haskell
• Python's built-in functions: A complete exploration. ~ Leodanis Pozo Ramos. #Python #Programming
• Introducing category theory. ~ Peter Smith. #CategoryTheory

Las lecturas compartidas en Mastodon el 1 de julio de 2024 son

• Lecturas compartidas el 30 de junio de 2024. #ITP #IsabelleHOL #Math #Haskell #Python
• Formalized synthetic geometry. ~ André Hernández-Espiet. #PhDThesis #ITP #Lean4 #Math
• Verification using formalised mathematics and theorem proving of reinforcement and deep learning. ~ Mark Chevallier. #ITP #IsabelleHOL #DeepLearning
• AI for Mathematics (AI4Math) paper list. ~ Haocheng Ju. #AI #Math #ITP #MachineLearning

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

• Lecturas compartidas el 29 de junio de 2024. #ITP #Lean4 #IsabelleHOL #PVS #Coq #Logic #Math #Haskell #Python
• #Exercitium: Conjunto de divisores. #Haskell #Python #Matemáticas
• The accompanying code for the submission "Formalising half of a graduate textbook on number theory" to ITP 2024. ~ Manuel Eberl, Anthony Bordg, Lawrence Paulson, and Wenda Li. #ITP #IsabelleHOL #Math
• Nine chapters of analytic number theory in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math

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