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

The readings shared in Bluesky on 30 December 2024 are

• Readings shared December 29, 2024. #Haskell #Python #Math #AI #ITP
• Formal verification of a custom scheduling algorithm and specification of a Round-Robin implementation using Coq. ~ Christian Choa et als. #ITP #Coq #Rocq
• Formal verification of shortest job first scheduling algorithm in Coq. ~ Jian Lawrence Luteria et als. #ITP #Coq #Rocq
• Rocq prover: A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more. #ITP #Rocq
• Generalized Dijkstra in Haskell. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Tutorial on good Lisp programming style. ~ Peter Norvig, Kent Pitman (1993). #CommonLisp #Programming
• Paradigms of artificial intelligence programming (Case studies in Common Lisp). ~ Peter Norvig. #eBook #AI #CommonLisp #Programming
• Emacs Lisp guide. ~ Chris Done. #Emacs #Lisp
• Category theory illustrated. ~ Jencel Panic. #CategoryTheory
• Mathematical expression and reasoning for computer science. ~ David Liu, Toniann Pitassi. #eBook #Logic #Math #CompSci
• How to use Emacs as a desktop environment in Linux with EXWM. ~ Ramces Red. #Emacs
• Historias de la IA: los autómatas. ~ Manuel de León. #IA #Autómatas

The readings shared in Bluesky on 29 December 2024 are

• Readings shared December 27, 2024. #ITP #IsabelleHOL #Math #Teaching #AI #LLMs #Emacs
• #Exercitium: Exponente en la factorización. #Haskell #Python #Matemáticas
• Machine-assisted proof. ~ Terence Tao. #Math #AI #ITP
• AMS Advisory Group on Artificial Intelligence. ~ Akshay Venkatesh, Mark C. Wilson. #Math #AI