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