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

The readings shared in Bluesky on 27 December 2024 are

• Readings shared December 26, 2024. #Haskell #Python #Math
• A generalization of the Cauchy–Davenport theorem (in Isabelle/HOL). ~ Mantas Bakšys. #ITP #IsabelleHOL #Math
• Formally verified approximate policy iteration. ~ Maximilian Schäffeler, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Myths of mathematics teaching. ~ Daniel J. Velleman. #Math #Teaching
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. #AI #LLMs #Math
• AI: Beyond the headlines (The hype surrounding artificial intelligence has created misconceptions that may lead to missed opportunities). ~ Erdin Beshimov. #AI
• Dibujando figuras con Emacs. ~ Notxor. #Emacs

The readings shared in Bluesky on 26 December 2024 are

• Readings shared December 25, 2024. #Haskell #Python #Math #ITP #LeanProver #Lean4 #Lisp #Programming
• #Exercitium: Reconocimiento de potencias de 4. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 25 December 2024 are

• Readings shared December 24, 2024. #ITP #Agda #Haskell #FunctionalProgramming #Haskell #Python #AI #LLMs #Math
• #Exercitium: El teorema de Navidad de Fermat. #Haskell #Python #Math
• Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• The bipolar Lisp programmer. ~ Mark Tarver. #Lisp #Programming

The readings shared in Bluesky on 24 December 2024 are

• Readings shared December 23, 2024. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization #Programming #JuliaLang #Python #MachineLearning #Golog #LogicProgramming
• #Exercitium: Producto de los elementos de la diagonal principal. #Haskell #Python #Matemáticas
• Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. #ITP #Math #Education
• Data for mathematical copilots: Better ways of presenting proofs for machine learning. ~ Simon Frieder et als. #AI #LLMs #Math
• Compiling dependent type preconditions to runtime checks with Agda2Hs. ~ Jakob Naucke. #ITP #Agda #Haskell #FunctionalProgramming

The readings shared in Bluesky on 23 December 2024 are

• Readings shared December 21, 2024. #ITP #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization
• Can AI do maths yet? Thoughts from a mathematician. ~ Kevin Buzzard. #AI #ITP #Math
• The state of Julia for scientific machine learning. ~ Edward Berman, Jacob Ginesin. #Programming #JuliaLang #Python #MachineLearning
• LTLf synthesis on first-order agent programs in nondeterministic environments. ~ Till Hofmann, Jens Claßen. #AI #Golog #LogicProgramming

The readings shared in Bluesky on 21 December 2024 are

• Readings shared December 20, 2024. #ITP #Mizar #Math #Haskell #Python #AI
• Isabelle quick start guide. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• An imperative programmer tries to learn Haskell. ~ Thane Thomson. #Haskell #FunctionalProgramming
• Solving perfect numbers quickly with Haskell. ~ Andrew MacGillivray. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 20 December 2024 are

• Readings shared December 19, 2024. #ITP #IsabelleHOL #Mizar #Logic #Math #Haskell #FunctionalProgramming #LLMs
• #Exercitium: Reiteración de suma de consecutivos. #Haskell #Python #Matemáticas
• Formalize the octonions. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Apriori knowledge in an era of computational opacity: The role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math