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

• Lecturas compartidas el 24 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "La equipotencia es una relación de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Mínimo producto escalar. #Haskell #Python #Matemáticas
• Teaching mathematics to computers. ~ Kevin Buzzard (@XenaProject). #ITP #Lean4 #Math #AI #MachineLearning
• Towards a formalized proof of Carleson's theorem. ~ Floris van Doorn. #ITP #Lean4 #Math
• Linear algebra game in Lean. ~ Sina Hazratpour. #ITP #Lean4 #Math
• Building measure theory using hierarchy builder. ~ Cyril Cohen. #ITP #Coq #Math
• Symbolic computation for all the fun. ~ Chad E. Brown, Mikoláš Janota, Mirek Olšák. #Math #ATP
• System introductions I: HOL (1). ~ Freek Wiedijk. #ITP #HOL
• More on HOL Light (2). ~ Freek Wiedijk. #ITP #HOL_Light
• Even more on HOL Light (3). ~ Freek Wiedijk. #ITP #HOL_Light
• Modularity in PVS. ~ Sam Owre. #ITP #PVS
• Lessons from Metamath. ~ Mario Carneiro. #ITP #Metamath
• A quick tour of Agda. ~ Guillaume Allais. #ITP #Agda
• Theorem proving and AI. ~ Josef Urban. #ATP #ITP #AI #Math
• System introductions I: Lean. ~ Mario Carneiro. #ITP #Lean4
• System introductions II: Isabelle. ~ Manuel Eberl. #ITP #IsabelleHOL
• System introductions: PVS. ~ Sam Owre. #ITP #PVS
• Reconciling type theory with the use of a single type of numbers for mathematical education at introductory levels. ~ Yves Bertot. #ITP #Coq #Math
• Programming mathematics: Tools and challenges. ~ Georges Gonthier. #ITP #Coq
• From informal to formal and back. ~ Patrick Massot. #ITP #Lean4 #Math
• Beautiful formalizations and proofs. ~ Natarajan Shankar. #ITP #PVS #Math
• Workshop: Formalization of Mathematics (June 2024). Hausdorff Center for Mathematics. #ITP #Math
• AI tools for Better Math. ~ Valeria de Paiva (@vcvpaiva@mathstodon.xyz). #Math #AI
• La grande épopée des algorithmes. ~ Claire Mathieu. #Algorithms