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

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 (@byorgey@mathstodon.xyz). #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