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

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

• Lecturas compartidas el 18 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Agda #Physics #Math #Programming #Python
• Libro "Calculemus (Demostraciones con Lean4)" (versión 18-mayo-24). #ITP #Lean4 #Math
• #Exercitium: Diferencia simétrica. #Haskell #Python #Matemáticas
• Bridging syntax and semantics of Lean expressions in E-Graphs. ~ Marcus Rossel and Andrés Goens. #ITP #Lean4
• PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL. ~ Andreas Viktor Hess, Sebastian Alexander Mödersheim, Achim D. Brucker and Anders Schlichtkrull. #ITP #IsabelleHOL
• Metamathematics. ~ David Marker. #Logic #Math

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

• Lecturas compartidas el 17 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (18-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Proofs and conversations. ~ Talia Ringer (@TaliaRinger@mathstodon.xyz). #ITP #Coq #Math
• Functional induction. ~ Joachim Breitner (@nomeata@mastodon.online). #ITP #Lean4
• HepLean: Digitalising high energy physics. ~ Joseph Tooby-Smith. #ITP #Lean4 #Physics
• Foundational verification of smart contracts through verified compilation. ~ Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao. #ITP #Coq
• Initial algebras unchained (A novel initial algebra construction formalized in Agda). ~ Thorsten Wißmann and Stefan Milius. #ITP #Agda #Math
• Programming as a mediator of mathematical thinking (Examples from upper secondary students exploring the definite integral). ~ Timo Tossavainen, Claes Johansson, Alf Juhlin and Anna Wedestig. #Math #Programming #Python
• Math databases. ~ Jeremy Kun (@j2kun@mathstodon.xyz). #Math
• code4math: Consortium of digital ecosystems for mathematics. #Math

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

• Lecturas compartidas el 16 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Logic #Math #FunctionalProgramming #Haskell #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)ⁿ". #ITP #Lean4 #IsabelleHOL #Math