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

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