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 (@PeterSmith@mathstodon.xyz). #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 (@LawrPaulson@mathstodon.xyz). #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 (@aarroyoc@castilla.social). #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 (@byorgey@mathstodon.xyz). #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 (@XenaProject). #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 (@vcvpaiva@mathstodon.xyz). #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