Las lecturas compartidas en Mastodon el 12 de mayo de 2024 son

• Lecturas compartidas el 11 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
• Libro "Calculemus (Demostraciones con Lean4)" (versión 11-mayo-24). #ITP #LeanProver #Lean4 #Matemáticas
• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #Lean4 #Math
• Agda core: The dream and the reality. ~ Jesper Cockx #ITP #Agda
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 11 de mayo de 2024 son

• Lecturas compartidas el 10 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #SAT_solver #FunctionalProgramming #Haskell #Python #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (11-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math
• Course: Formalising Mathematics in Lean. ~ Adrián Doña Mateo, Monica Abu Omar, Patrick Kinnear and Simone Castellan. #ITP #Lean4 #Math
• Course: Formalized Mathematics in Lean (Winter 23/24). ~ Floris van Doorn. #ITP #Lean4 #Math
• Course: Theorem proving with Lean. ~ Damiano Testa. #ITP #Lean4 #Math
• Partial correctness of the top-down solver (in Isabelle/HOL). ~ Yannick Stade, Sarah Tilscher, Helmut Seidl. #ITP #IsabelleHOL
• LL(1) parser generator (in Isabelle/HOL). ~ Sarah Tilscher and Simon Wimmer. #ITP #IsabelleHOL
• How to explore Lisp metaprogramming techniques. #CommonLisp
• The way of Lisp or the right way. ~ Joe Marshall. #Lisp #Programming

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

• Lecturas compartidas el 9 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #CategoryTheory
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de la unicidad del elemento neutro en los grupos. #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Diagonales principales de una matriz. #Haskell #Python #Matemáticas
• Verifying a SAT solver from ground up. ~ Mathias Fleury. #ITP #IsabelleHOL #SAT_solver
• Solving recurrence relations. ~ John Mount. #Python #Math

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

• Lecturas compartidas el 8 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces a⋅b = a ↔ b = 1". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #Matemáticas
• Compiling higher order functions with GADTs. ~ Srijan. #FunctionalProgramming #Haskell
• When are functions lazy enough for lists. ~ Daniel Beskin. #FunctionalProgramming #Haskell
• Notes on Category Theory (with examples from basic mathematics). ~ Paolo Perrone. #CategoryTheory

Las lecturas compartidas en Mastodon el 8 de mayo de 2024 son

• Lecturas compartidas el 7 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #SMT #Logic #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide conmutativo y x, y, z ∈ M tales que x⋅y = 1 y x⋅z = 1, entonces y = z.". #ITP #Lean4 #IsabelleHOL #Math
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• HOL4P4: Mechanized small-step semantics for P4. ~ Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam. #ITP #HOL4

Las lecturas compartidas en Mastodon el 7 de mayo de 2024 son

• Lecturas compartidas el 6 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #AI #LLMs #Programming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Sea M un monoide y a, b ∈ M tales que ab = 1. Entonces, a = 1 si y sólo si b = 1". #ITP #Lean4 #IsabelleHOL #Math
• Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. #ITP #Agda #Math
• NL2FOL: Translating natural language to first-order logic for logical fallacy detection. ~ Abhinav Lalwani, Lovish Chopra, Christopher Hahn, Caroline Trippel, Zhijing Jin, Mrinmaya Sachan. #LLMs #SMT #Logic

Las lecturas compartidas en Mastodon el 6 de mayo de 2024 son

• Lecturas compartidas el 5 de mayo de 2024. #ITP #IsabelleHOL #Lean4 #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide, x ∈ M y m, n ∈ N, entonces x^(m+n)=x^m · x^n". #ITP #Lean4 #IsabelleHOL #Math
• Formalizing Pick's theorem in Isabelle/HOL. ~ Sage Binder, Katherine Kosaian. #ITP #IsabelleHOL #Math
• Guided equality saturation. ~ Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer. #ITP #Lean4
• An introduction to MathComp-Analysis. ~ Reynald Affeldt. #ITP #Coq #Math
• Formalizing soundness proofs of linear PCP SNARKs. ~ Bolton Bailey, Andrew Miller. #ITP #Lean4
• Automatic programming: Large language models and beyond. ~ Michael R. Lyu, Baishakhi Ray, Abhik Roychoudhury, Shin Hwei Tan, Patanamon Thongtanunam. #LLMs #Programming

Las lecturas compartidas en Mastodon el 5 de mayo de 2024 son

• Lecturas compartidas el 4 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #AI
• Libro "Calculemus (Demostraciones con Lean4)" (versión 4-mayo-24). #ITP #LeanProver #Lean4 #Matemáticas
• Verification and refinement of natural language explanations through LLM-symbolic theorem proving. ~ Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas. #AI #LLMs #ITP #IsabelleHOL

Las lecturas compartidas en Mastodon el 4 de mayo de 2024 son

• Lecturas compartidas el 3 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #CompSci #Education #AI #GenerativeAI #MachineLearning #DeepLearning
• Libro "Piensa en Haskell y en Python" (versión del 3-may-24). #Haskell #Python #Matemáticas #Algorítmica
• Resumen de lecturas compartidas durante abril de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (4-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Substitutions for lambda-free higher-order terms (in Isabelle/HOL). ~ Vincent Trélat. #ITP #IsabelleHOL
• A narrative history of Artificial Intelligence. ~ Masayuki Ida. #AI