The readings shared in Mastodon on 22 October 2024 are

• Readings shared October 21, 2024. #ITP #LeanProver #Lean4 #Coq #Math #AI #AI4Mat #Emacs #Lisp
• Kripke-style semantics for strong functors. ~ Nachiappan Valliappan. #ITP #Agda
• Analysis on normed semirings and semimodules. ~ Matt Verhoeven. #ITP #Coq #Math
• An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain. ~ Byron Cook. #ITP
• Neural approaches to theorem search & proof repair. ~ Thomas Reichel. #ITP #Coq #LLMs
• Towards Guaranteed Safe AI: A framework for ensuring robust and reliable AI systems. ~ David Dalrymple et als. #AI

The readings shared in Mastodon on 21 October 2024 are

• Readings shared October 20, 2024. #ITP # #LambdaCalculus #FunctionalProgramming #ALP #LogicProgramming #AI #LLMs #Math
• The Lean Language Reference. #ITP #LeanProver #Lean4
• Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies.][]]AI for Mathematics paper list. #AI #Math #AI4Mat #ITP #Coq #Math
• Safeguarded AI: this programme aims to develop the safety standards we need for transformational AI. #AI
• Mathematics for Safe AI. ~ David Dalrymple. #AI
• Safeguarded AI: constructing guaranteed safety (Programme thesis). ~ David Dalrymple. #AI
• ProvablySafe.AI: a collaborative landing page for the field and community at the intersection of AI safety and formal methods. #AI
• Curso de Emacs Lisp. ~ Andros Fenollosa. #Emacs #Lisp
• Curso de Emacs Lisp orientado a las interfaces de usuario. ~ Andros Fenollosa. #Emacs #Lisp

The readings shared in Mastodon on 20 October 2024 are

• Readings shared October 20, 2024. #ITP #LeanProver #Lean4 #Math #Math #SetTheory #AI
• Foreign function verification through metaprogramming. ~ Joomy Korkut. #ITP #Coq
• Lecture notes on overview and the lambda calculus. ~ Jan Hoffmann. #LambdaCalculus
• Course: Types and Programming Languages. ~ Jan Hoffmann. #FunctionalProgramming
• An efficient propositional system for Abductive Logic Programming. ~ M. Gavanelli, P. Julián-Iranzo, F. Sáenz-Pérez. #ALP #LogicProgramming
• The accepted papers for the MATH-AI workshop have been released on OpenReview. #ITP #AI #LLMs #Math

The readings shared in Mastodon on 19 October 2024 are

• Readings shared October 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #Logic #Math #FunctionalProgramming #Prolog #LogicProgramming #Autoformalization #Emacs #Lisp
• ENS-Lean-course: Plain structures in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: How to build hierarchy of algebraic structures in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• Axiomatic set theory (Version of 18 October 2024). ~ Tom Leinster. #Math #SetTheory
• Nobel prizes and AI: The promise, the peril, and the path forward. ~ Marc Rotenberg. #AI

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. #ITP #Agda #Math
• Deep dive: The profound connection between Prolog and Lean (A technical analysis). ~ Alireza Dehbazargi. #Prolog #LogicProgramming #LeanProver #ITP
• Wooley's discrete inequality (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki. #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. #Logic
• Write your own Emacs Lisp macros - a short introduction. ~ Marie K. Ekeberg. #Emacs #Lisp

The readings shared in Mastodon on 17 October 2024 are

• Readings shared October 16, 2024. #AI #Education #FunctionalProgramming #Haskell #ITP #Lean4 #MachineLearning #Math1
• The Haskell Unfolder Episode 34: You already understand monads. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Ollama-haskell: Haskell bindings for Ollama. ~ Tushar Adhatrao. #Haskell #FunctionalProgramming #Ollama #LLMs
• Big advance on simple-sounding math problem was a century in the making. ~ Erica Klarreich. #Math
• Thinking about 12 aspects of personal information/knowledge management. ~ Sacha Chua. #Emacs #OrgMode
• Manual en español de GNU/Emacs 29.1. ~ Tano. #Emacs

The readings shared in Mastodon on 16 October 2024 are

• Readings shared October 15, 2024. #AI #ChatGPT #Emacs #FunctionalProgramming #GeoGebra #Haskell #ITP #LambdaCalculus #Lean4 #LeanProver #LogicProgramming #Math #OrgMode #Prolog
• Lean: First steps (13 - Disquality). ~ Tariq Rashid #ITP #Lean4 #Math
• Munihac WASM experiment: convert Haskell expressions to pointfree in your browser. ~ Sergey Vinokurov. #Haskell #FunctionalProgramming
• Por qué debemos enseñar Machine Learning en todos los títulos universitarios. ~ Manuel de León Rodríguez y Rodrigo Trujillo González. #Education #AI #MachineLearning

The readings shared in Mastodon on 15 October 2024 are

• Readings shared October 13, 2024. #AI #CategoryTheory #Coq #Education #FunctionalProgramming #Haskell #ITP #ITP
• On using GeoGebra and ChatGPT for geometric discovery. ~ Francisco Botana, Tomás Recio, María Pilar Vélez. #GeoGebra #ChatGPT #Math #AI
• Lean: First steps (12 - Odd & Even ). ~ Tariq Rashid #ITP #Lean4 #Math
• Tutorial videos for the course "Lean: First Steps". ~ Tariq Rashid. #ITP #Lean4 #Math
• The handshaking lemma. ~ Christoph Spiegel. #ITP #LeanProver #Lean4 #Math
• Water sort in Haskell. ~ Nicolas Audinet de Pieuchon. #Haskell #FunctionalProgramming
• The power of Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Programación lógica con restricciones. #Prolog #LogicProgramming
• Emacs para ciencias del dato. #Emacs #OrgMode
• The λ-calculus, 2: The Church-Rosser theorem. ~ Lawrence Paulson. #LambdaCalculus

The readings shared in Mastodon on 13 October 2024 are

• Readings shared October 12, 2024. #AI #ATP #IMO #ITP #LLMs #Lean4 #MachineLearning #Math #SetTheory
• Effects and coeffects in call-by-push-value. ~ Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich. #ITP #Coq
• Fully verified instruction scheduling. ~ Ziteng Yang, Jun Shirako, Vivek Sarkar. #ITP #Coq
• Iris-MSWasm: Elucidating and mechanising the security invariants of memory-safe WebAssembly. ~ Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal. #ITP #Coq
• Hazel: a live functional programming environment organized around typed holes. ~ Cyrus Omar et als. #ITP #FunctionalProgramming #Hazel
• Learner-centered design criteria for classroom proof assistants. ~ Matthew Keenan, Cyrus Omar. #ITP #Hazel
• Accessible bridge between category theory and functional programming. ~ Fethi Kadhi. #Haskell #FunctionalProgramming #CategoryTheory
• Refinement type refutations. ~ Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala. #Haskell #FunctionalProgramming
• Intensional functions. ~ Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu. #Haskell #FunctionalProgramming
• Semantics lifting for syntactic sugar. ~ Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu. #Haskell #FunctionalProgramming
• The use of artificial intelligence in teaching students programming languages. ~ Svitlana Lytvynova, Natalya Rashevska and Svitlana Proskura. #AI #Education #Programming

The readings shared in Mastodon on 12 October 2024 are

• Readings shared October 11, 2024. #ITP #LeanProver #Coq #Deduce #IsabelleHOL #Math #LLMs #LogicProgramming
• ENS-Lean-course: Functions in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Taxicab number in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• IMOSLLean4: Formalization of IMO shortlist problems in Lean 4. ~ Gian Sanjaya. #ITP #Lean4 #Math #IMO
• AI for Mathematics. ~ Jeremy Avigad. #ITP #LeanProver #ATP #AI #MachineLearning #LLMs #Math
• Axiomatic set theory (Version of 9 October 2024). ~ Tom Leinster. #Math #SetTheory