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 (@byorgey@mathstodon.xyz). #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 (@Marcelolaza). #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 (@rzeta0@mastodon.social). #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.f#page=61 #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 (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming