Las lecturas compartidas en Mastodon el 10 de agosto de 2024 son

• Lecturas compartidas el 9 de agosto de 2024. #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA
• Function composition and currying in Python (Python in the streets, Haskell in the sheets!). ~ Francisco Gutierrez. #Python #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 9 de agosto de 2024 son

• Lecturas compartidas el 8 de agosto de 2024. #ITP #Lean4 #IsabelleHOL #Math #DeepLearning
• A tricky lower bound proof. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Verified transformations for convex programming. ~ Ramon Fernández Mir. #ITP #Lean4 #Math
• First steps towards computational polynomials in Lean. ~ James Harold Davenport. #ITP #LeanProver #Math
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner & Detlef Plump. #ITP #IsabelleHOL
• Validation of a formal floating-point model for the interactive proof assistant Isabelle/HOL. ~ Olof Lindström. #ITP #IsabelleHOL
• Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. #ITP #HOL4
• An in-context learning agent for formal theorem-proving. ~ Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri. #LLMs #ITP #Coq #LeanProver
• Competitive programming in Haskell: Tree path decomposition, part II. ~ Brent Yorgey (@byorgey@mathstodon.xyz). #Haskell #FunctionalProgramming
• typedKanren: Statically typed relational programming with exhaustive matching in Haskell. ~ Nikolai Kudasov & Artem Starikov. #Haskell #FunctionalProgramming
• Combinatorial and algorithmic mathematics (From foundation to optimization) ~ Baha M. Alzalg #Math
• Intelligent Computer Mathematics (17th International Conference, CICM 2024, Proceedings) #ITP #Math
• The potential for AI in science and mathematics. ~ Terence Tao. #IA #Math #ITP #LeanProver

Las lecturas compartidas en Mastodon el 08 de agosto de 2024 son

• Lecturas compartidas el 6 de agosto de 2024. #ITP #Coq #Python #FunctionalProgramming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length(xs ++ ys) = length(xs) + length(ys)". #ITP #Lean4 #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si. #ITP #DeepLearning
• Getting started with Blueprint-Driven formalization projects in Lean. ~ Pietro Monticone (@PietroMonticone). #ITP #LeanProver #Lean4

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 (@lysxia). #FunctionalProgramming #Hope #Miranda
• Analyzing Haskell stability. ~ Jappie Klooster (@jappieklooster). #Haskell #FunctionalProgramming
• Data.Maybe, and thoughts on library design. ~ Srijan Paul (@_injuly). #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 (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #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