The readings shared in Mastodon on August 15, 2024 are

• Readings shared August 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• Software verification with Isabelle/HOL. ~ Peter Höfner. #ITP #IsabelleHOL
• Functional algorithms verified in SSReflect. ~ Alex Gryzlov et als. #ITP #Coq #SSReflect
• Haskell for Elm developers: giving names to stuff (Part 5 - Semigroups and Monoids). ~ Flavio Corpa (@FlavioCorpa). #Haskell #Elm #FunctionalProgramming
• The Haskell Unfolder Episode 31: nothunks. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming
• Galois theory. ~ Tom Leinster. #Math

The readings shared in Mastodon on August 14, 2024 are

• Readings shared August 13, 2024. #ITP #Coq #Agda #Math #Python
• #Calculemus: Proofs with Lean4 and Isabelle/HOL of "take n xs ++ drop n xs = xs". #ITP #Lean4 #IsabelleHOL #Math
• Introduction to proofs with Lean proof assistant. ~ Sina Hazratpour (@sina_htpr). #ITP #LeanProver
• Taller de Lean 4. ~ Enric Cosme, Mario Vago. #ITP #LeanProver #Lean4
• A topological approach for semi-supervised learning. ~ Adrián Inés, César Domínguez, Jónathan Heras, Gadea Mata & Julio Rubio. #AI #MachineLearning #Math

The readings shared in Mastodon on August 13, 2024 are

• Readings Shared August 13, 2024. #Python #Haskell #FunctionalProgramming
• An elementary proof of the FMP for Kleene algebra. ~ Tobias Kappé. #ITP #Coq #Math
• Sharing proofs with predicative theories through universe-polymorphic elaboration. ~ Thiago Felicissimo & Frédéric Blanqui. #ITP #Agda #Coq
• Bounding Euler's constant. ~ Philip Zucker (@sandmouth@types.pl). #Math #Python
• Algebra. It's powerful. But it's not what it was. ~ Keith Devlin (@KeithDevlin@fediscience.org). #Math

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