The readings shared in Bluesky on 11 January 2025 are

• Readings shared January 10, 2025. #ITP #LeanProver #Logic #Math #Haskell #Python #ASP #LogicProgramming #AI #NeuroSymbolicAI #LLMs
• #Exercitium: Números amigos. #Haskell #Python #Matemáticas
• Categories and Haskell (An introduction to the mathematics behind modern functional programming). ~ Jan-Willem Buurlage. #CategoryTheory #Haskell #FunctionalProgramming
• LeanUniverse: A library for consistent and scalable Lean4 dataset management. ~ Aram H. Markosyan, Gabriel Synnaeve, Hugh Leather. #ITP #LeanProver
• Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre Corbineau, Basile Gros, Jean-François Monin. #ITP #Coq #Rocq
• On the correctness of Barron and Strachey’s cartesian product function. ~ Wouter Swierstra, Jason Hemann. #Haskell #FunctionalProgramming #ITP #Agda
• Alpha beta pruning with the selection monad. ~ Johannes Hartmann, Jeremy Gibbons. #Haskell #FunctionalProgramming
• Using GHC core to normalise student programs. ~ Matilda Blomqvist, Alex Gerdes. #Haskell #FunctionalProgramming
• Shallowly embedded functions. ~ Mart Lubbers, Pieter Koopman, Niek Janssen. #Haskell #FunctionalProgramming
• CoScheme: Compositional copatterns in Scheme. ~ Paul Downen, Adriano Corbelino II. #FunctionalProgramming
• Assessment in computer science education in the GenAI era (Prioritizing critical thinking over syntax mastery). ~ Orit Hazzan. #ComputerSci #Education #GenAI

The readings shared in Bluesky on 10 January 2025 are

• Readings shared January 9, 2025. #ITP #LeanProver #Logic #Math #FunctionalProgramming #Haskell #JavaScript #Python #AI #NeuralNetwork #ChatGPT
• #Exercitium: Máxima suma de caminos en un triángulo. #Haskell #Python #Matemáticas
• Teaching "Foundations of mathematics" with the LEAN theorem prover (Master's Thesis). #ITP #LeanProver #Logic #Math
• Learning to automatically solve logic grid puzzles. ~ Arindam Mitra, Chitta Baral (2015). #ASP #LogicProgramming
• Neuro-symbolic AI in 2024: A systematic review. ~ Brandon C. Colelough, William Regli. #AI #NeuroSymbolicAI
• Un comparador de modelos de Inteligencia Artificial. ~ @Alvy. #AI #LLMs

The readings shared in Bluesky on 9 January 2025 are

• Readings shared January 8, 2025. #ITP #IsabelleHOL #AI #MachineLearning #LLMs
• Teaching "Foundations of mathematics" with the LEAN theorem prover. ~ Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Using a JavaScript component inside a Haskell application. ~ Mateusz Goślinowski. #Haskell #FunctionalProgramming #JavaScript
• Mathematics of neural networks (Lecture notes graduate course). ~ Bart M.N. Smets. #NeuralNetwork #Math
• Notes on mathematical logic (Vol. 1). ~ David W. Kueker. #Logic #Math
• Notes on mathematical logic (Vol. 2). ~ David W. Kueker. #Logic #Math
• ChatGPT: Cómo hacer (y mejorar) mi Trabajo de Fin de Carrera de la Universidad en un par de minutos. ~ Chema Alonso. #ChatGPT #Python #Programming

The readings shared in Bluesky on 8 January 2025 are

• Readings shared January 6, 2025. #ITP #IsabelleHOL #LeanProver #Lean4 #Agda #Coq #Rocq #HoTT #Math #AI #LLMs
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• Can AI models reason like a human? ~ Wayne Joubert. #AI #LLMs
• Artificial intelligence then and now (From engines of logic to engines of bullshit?). ~ Thomas Haigh. #AI #MachineLearning #LLMs

The readings shared in Bluesky on 6 January 2025 are

• Readings shared January 4, 2025. #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python
• Computing huge Fibonacci numbers, by proof and by code. ~ Lawrence Paulson. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #LeanProver #Lean4 #Math
• Mathematicians found – and fixed – an error in a 60-year-old proof. ~ Alex Wilkins.L#selection-733.0-733.66 #ITP #LeanProver #Math
• Large language models for mathematical analysis. ~ Ziye Chen, Hao Qi. #AI #LLMs #Math
• On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. #ITP #Agda #HoTT
• Laws of quantum programming. ~ Mingsheng Ying, Li Zhou, Gilles Barthe. #ITP #Coq #Rocq #QuantumProgramming
• El libro recursivo de la recursividad. ~ @Alvy. #Programación

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 2, 2025. #Haskell #Python #Math
• #Exercitium: Mayor órbita de la sucesión de Collatz. #Haskell #Python #Matemáticas
• Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Décomposition algébrique cylindrique en Coq/Rocq. ~ Quentin Vermande. #ITP #Coq #Rocq #Math
• Formalizing adhesive category theory in Rocq. ~ Samuel Arsac, Russell Harmer, Damien Pous. #ITP #Rocq
• Vérification de bout en bout d’une fonction de bibliothèque mathématique. ~ Paul Geneau de Lamarlière. #ITP #Coq #Rocq #Math
• Safe external calls from formally verified functional code: exiting the monad, and a BDD case study. ~ David Monniaux, Sylvain Boulmé. #ITP #Coq #Rocq
• Modular probabilistic programming with algebraic effects. ~ Oliver Goldstein, Ohad Kammar. #Haskell #FunctionalProgramming
• Parallel QuickHull algorithm in Haskell. ~ George Morgulis, Henry Lin. #Haskell #FunctionalProgramming
• Parallel SAT solver. ~ Yixuan Li, Jiaqian Li, Phoebe Wang. #Haskell #FunctionalProgramming
• Storable types: free, absorbing, custom. ~ Basile Clément, Camille Noûs, Gabriel Scherer. #OCaml #FunctionalProgramming
• Typechecking of overloading in programming languages and mechanized mathematics. ~ Arthur Charguéraud, Martin Bodin, Louis Riboulet. #OCaml #FunctionalProgramming
• Applying machine learning to number-theoretical data (A focus on class groups of imaginary quadratic fields). ~ Hugo Sträng. #AI #MachineLearning #Math

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 3, 2025. #ITP #Lean4 #IsabelleHOL #Coq #Rocq #Math #FunctionalProgramming #OCaml #Haskell #Python #AI #MachineLearning
• #Exercitium: Caminos en un triángulo. #Haskell #Python #Matemáticas
• Demostraciones con Isabelle/HOL del "Praeclarum theorema" de Leibniz. #ITP #IsabelleHOL #Logic
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als.. #ITP #LeanProver #Math
• Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. #ITP #HOL_Light #Logic
• Ascoli-Arzel`a theorem (Metric space version). ~ Keiichi Miyajima, Hiroshi Yamazaki. #ITP #Mizar #Math
• Universality of measure space. ~ Noboru Endou, Yasunari Shidama. #ITP #Mizar #Math
• Formalization of orthogonal complements of normed spaces. ~ Hiroyuki Okazaki. #ITP #Mizar #Math

The readings shared in Bluesky on 2 January 2025 are

• Readings shared January 1, 2025. #ITP #LeanProver #Lean4 #Mizar #Math #Haskell #Python
• #Exercitium: Ternas pitagóricas con suma dada. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 1 January 2025 are

• Readings shared December 31, 2024. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Formal proof of transcendence of the number e (Part I). ~ Yasushige Watase. #ITP #Mizar #Math
• Formal proof of transcendence of the number e (Part II). ~ Yasushige Watase. #ITP #Mizar #Math
• #Exercitium: Suma de múltiplos de 3 o de 5. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 31 December 2024 are

• Readings shared December 30, 2024. #ITP #Coq #Rocq #FunctionalProgramming #Haskell #CommonLisp #EmacsLisp #Emacs #Logic #Math #CategoryTheory #AI
• A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL