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

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

• Lecturas compartidas el 23 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Math #AI
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Los supremos de las sucesiones crecientes son sus límites". #ITP #Lean4 #IsabelleHOL #Math
• Towards mechanised consensus in Isabelle. ~ Elliot Jones and Diego Marmsoler. #ITP #IsabelleHOL
• Towards formally specifying and verifying smart contract upgrades in Coq. ~ Derek Sorensen. #ITP #Coq

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

• Lecturas compartidas el 22 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva". #ITP #Lean4 #IsabelleHOL #Math
• VOLPIC: Verifying lifted Pascal in Coq. ~ Charles Averill. #ITP #Coq
• The Haskell Unfolder Episode 26: Variable-arity functions. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming
• Why mathematics is set to be revolutionized by AI. ~ Thomas Fink. #Math #AI
• Online historical maths textbooks. #Math

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

• Lecturas compartidas el 21 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #SMT #Z3 #FunctionalProgramming #Haskell #Python #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si una función es creciente e involutiva, entonces es la identidad". #ITP #Lean4 #IsabelleHOL #Math

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

• Lecturas compartidas el 20 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La composición de una función creciente y una decreciente es decreciente". #ITP #Lean4 #IsabelleHOL #Math
• On the ingredients for Fermat. ~ Kevin Buzzard. #ITP #Lean4 #Math
• Quiver: Guided abductive inference of separation logic specifications in Coq. ~ Simon Spies, Lennard Gäher, Michael Sammler and Derek Dreyer. #ITP #Coq
• Proving Sum n = n*(n-1)/2 and that 1/n tends to 0. ~ Philip Zucker (@sandmouth@types.pl). #Python #SMT #Z3
• Prefer do notation over Applicative operators when assembling records. ~ Gabriella Gonzalez (@GabriellaG439).l#FunctionalProgramming #Haskell
• Beauty is not simplicity: An analysis of mathematicians' proof appraisals. ~ Matthew Inglis and Andrew Aberdein. #Math

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

• Lecturas compartidas el 19 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Haskell #Python #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Los monoides booleanos son conmutativos". #ITP #Lean4 #IsabelleHOL #Math
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Linear resources in Isabelle/HOL. ~ Filip Smola and Jacques D. Fleuriot. #ITP #IsabelleHOL
• Grothendieck's use of equality. ~ Kevin Buzzard. #Math #ITP #LeanProver
• Beyond trees: Calculating graph-based compilers. ~ Patrick Bahr and Graham Hutton. #FunctionalProgramming #Haskell