The readings shared in Bluesky on 16 January 2025 are

• Readings shared January 15, 2025. #ITP #LeanProver #Logic #Math #CompSci #FunctionalProgramming #Haskell
• #Exercitium: Sucesión de números amigos. #Haskell #Python #Matemáticas
• #Exercitium: Suma de los números amigos menores que n. #Haskell #Python #Matemáticas
• Game "An introduction to constructive logic". ~ Mark Fischer et als./#/g/trequetrum/lean4game-logic #ITP #LeanProver #Logic
• Vertex algebras in Mathlib: coming soon? ~ Scott Carnahan. #ITP #LeanProver #Math
• Real world autoformalization. ~ Siddhartha Gadgil. #ITP #LeanProver #Math
• Building a formal verification framework for smart contracts. ~ Jakob von Raumer. #ITP #LeanProver
• The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? ~ Jason Rute. #ITP #LeanProver #AI
• Information theory in Lean: the DPI. ~ Lorenzo Luccioli. #ITP #LeanProver
• A nimble introduction to nimbers. ~ Violeta Hernández Palacios. #ITP #LeanProver #Math
• An agda2hs-compatible representation of exact real arithmetic. ~ Viktor Csimma. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating SAT and SMT solvers on large-scale sudoku puzzles. ~ Liam Davis, Tairan Ji. #SAT #SMT
• The Haskell Unfolder Episode 38: tasting and testing CUDA (map, fold, scan). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• U-MATH: A university-level benchmark for evaluating mathematical skills in LLMs. ~ Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, Alex Myasnikov, Vlad Stepanov, Alexei Miasnikov, Sergei Tilga. #LLMs #Math