Las lecturas compartidas en Mastodon el 2 de junio de 2024 son

• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (2-junio-24). #ITP #Lean4 #IsabelleHOL #Math
• Intro to Lean 4: A language at the intersection of programming and mathematics. ~ Kiiya. #ITP #Lean4
• A boolean is maybe true. ~ Håkon Robbestad Gylterud. #FunctionalProgramming #Haskell
• Principles of dependent type theory. ~ Carlo Angiuli and Daniel Gratzer (@danielgratzer@mathstodon.xyz). #TypeTheory #FunctionalProgramming
• L’intelligence artificielle : Hier, aujourd’hui … et demain. ~ Jean-Paul Haton. #IA

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

• Lecturas compartidas el 30 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ". #ITP #Lean4 #IsabelleHOL #Math
• Liquid Haskell through the compilers. ~ Facundo Domínguez. #FunctionalProgramming #LiquidHaskell

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

• Lecturas compartidas el 29 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y". #ITP #Lean4 #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Formalization of asymptotic convergence for stationary iterative methods. ~ Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin. #ITP #Coq #Math
• Certification of tail recursive bubble–sort in Theorema and Coq. ~ Isabela Dramnesc, Tudor Jebelean, and Sorin Stratulat. #ITP #Coq #Theorema
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk. #ATP #Prover9
• Automated theorem proving for Prolog verification. ~ Fred Mesnard, Thierry Marianne and Etienne Payet. #ATP #Vampire #TPTP #Prolog
• Free foil: Generating efficient and scope-safe abstract syntax. ~ Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. #FunctionalProgramming #Haskell
• Automated theorem provers help improve large language model reasoning. ~ Lachlan McGinness and Peter Baumgartner. #LLMS #ATP

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

• Lecturas compartidas el 27 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Autoformalisation #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La paradoja del barbero". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Descomposiciones triangulares. #Haskell #Python #Matemáticas
• IsarMathLib 1.30.0: Modules and update to Isabelle2024. #ITP #Isabelle #Math

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

• Lecturas compartidas el 26 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones convergentes están acotadas". #ITP #Lean4 #IsabelleHOL #Math
• Autoformalizing euclidean geometry. ~ Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si. #Autoformalisation #LLMs #ITP #Lean4
• Coding in Haskell: Writing and debugging megaparsec parsers for grep. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 26 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Go #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Un número es par si y solo si lo es su cuadrado". #ITP #Lean4 #IsabelleHOL #Math
• Proofs for a price: Tomorrow’s ultra-rigorous mathematical culture. ~ Silvia De Toffoli. #Math #ITP
• Poincaré on the value of reasoning machines. ~ Colin McLarty. #Math #ITP
• AlephZero and mathematical experience. ~ Simon DeDeo. #Math #AI #ITP
• Working with machines in mathematics. ~ Alex Davies. #Math #MachineLearning
• Automated mathematics and the reconfiguration of proof and labor. ~ Rodrigo Ochigame. #Math #ITP
• Machine Learning and Information Theory Concepts towards an AI Mathematician. ~ Yoshua Bengio and Nikolay Malkin. #Math #AI #ITP
• How to calculate pi in a new way. ~ Mahdi Sasar (@MahdiSasar@mathstodon.xyz). #Math

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

• Lecturas compartidas el 25 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #LLMs #MachineLearning
• Libro "Calculemus (Demostraciones con Lean4)" (versión 25-mayo-24). #ITP #Lean4 #Math
• Generating executable Go code from the Isabelle theorem prover. ~ Matthias Stübinger. #ITP #IsabelleHOL #Go

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

• Lecturas compartidas el 24 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math
• #Exercitium: Conjunto de primos relativos. #Haskell #Python #Matemáticas
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (25-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Statically typed functional programming with Python 3.12. ~ Oskar Wickström (@owickstrom). #FunctionalProgramming #Python
• Proving theorems recursively. ~ Haiming Wang et als. #ITP #IsabelleHOL #LLMs #MachineLearning
• DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. ~ Huajian Xin et als. #LLMs #ITP #Lean4