The readings shared in Mastodon on 18 October 2024 are

• Readings shared October 17, 2024. #Haskell #FunctionalProgramming #Ollama #LLMs #Math #Emacs #OrgMode
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #Lean4 #ITP #FunctionalProgramming #Math
• Basic probability in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Math
• A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Riccardo Brasca, Christopher Birkbeck, Eric Rodriguez Boidi, Alex Best, Ruben van De Velde, Andrew Yang. #ITP #LeanProver #Math
• Agda proof of the Knaster-Tarski Fixpoint Theorem. ~ Reed Mullanix (@totbwf@types.pl). #ITP #Agda #Math
• Deep dive: The profound connection between Prolog and Lean (A technical analysis). ~ Alireza Dehbazargi (@BDehbozorgi83). #Prolog #LogicProgramming #LeanProver #ITP
• Wooley's discrete inequality (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki (@angelikikoutso1@bird.makeup). #ITP #IsabelleHOL #Math
• Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies. #ITP #Coq #Math
• FormalAlign: Automated alignment evaluation for autoformalization. ~ Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, Zhijiang Guo. #Autoformalization #ITP #Lean4
• Improving Isabelle/VSCode: Towards better prover IDE integration via language server. ~ Thomas Lindae. #ITP #IsabelleHOL
• Course: Logic & algorithms. ~ Bob Atkey (@bentnib@types.pl). #Logic
• Write your own Emacs Lisp macros - a short introduction. ~ Marie K. Ekeberg. #Emacs #Lisp