The readings shared in Mastodon on 5 November 2024 are

• Readings shared November 4, 2024. #ITP #Lean4 #Math
• Functors to Monads: A story of shapes. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 4 November 2024 are

• Readings shared November 3, 2024. #Haskell #FunctionalProgramming
• Lean: First steps (14 - Disequality again)​ (Video). ~ Tariq Rashid. #ITP #Lean4 #Math

The readings shared in Mastodon on 3 November 2024 are

• Readings shared November 2, 2024. #ITP #LeanProver #IsabelleHOL #Coq #Math #SetTheory #CategoryTheory #AI #LLMs #Autoformalization
• Competitive programming in Haskell: Union-find. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 2 November 2024 are

• Readings shared November 1, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #Haskell #FunctionalProgramming #Autoformalization #LLMs
• The future of Mathematics in a world of machines. ~ Simone Severini. #Math #ITP #LeanProver #AI #LLMs #Autoformalization
• AIPS: An Olympiad-level AI system for algebraic inequalities. #LLMs #ITP #Lean4 #Math
• Proving the existence of stable assignments in democratic forking using Isabelle/HOL. ~ Jan-Georg Smaus. #ITP #IsabelleHOL
• Verified parser- and printer-combinator bidefinition in the Isabelle proof assistant. ~ Matthias Sleurink. #ITP #IsabelleHOL
• The Boustrophedon transform, the Entringer numbers, and related sequences (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici, Nobuko Yoshida. #ITP #Coq
• Axiomatic set theory (Version of 31 October 2024). ~ Tom Leinster. #Math #SetTheory
• Basic category theory. ~ Tom Leinster. #Math #CategoryTheory
• Computational thinking: The idea that lived. ~ Shuchi Grover. #Education #Programming

The readings shared in Mastodon on 1 November 2024 are

• Readings shared October 31, 2024. #ITP #IsabelleHOL #Lean4 #Coq #Math #GenerativeAI
• Intuitionistic propositional logic in Lean. ~ Dafina Trufaş. #ITP #Lean4 #Logic #Math
• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #Coq #LLMs
• Going REPLing with Haskeline. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Proving Olympiad algebraic inequalities without human demonstrations. ~ Chenrui Wei, Mengzhou Sun, Wei Wang. #LLMs #ITP #Math
• Autoformalize mathematical statements by symbolic equivalence and semantic consistency. ~ Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma. #Autoformalization #LLMs #IsabelleHOL #Math

The readings shared in Mastodon on 31 October 2024 are

• Readings shared October 30, 2024. #ITP #Lean4 #IsabelleHOL #Math #ITP #Prolog #ASP #LogicProgramming #LambdaCalculus #AI #LLMs
• Lean: First steps (14 - Disequality again)​. ~ Tariq Rashid. #ITP #Lean4 #Math
• Babai’s nearest plane algorithm (in Isabelle/HOL). ~ Eric Ren, Sage Binder, Katherine Kosaian. #ITP #IsabelleHOL #Math
• Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math #Education
• Generative AI as an icebreaker to help us accept other ways of thinking. ~ Berry Billingsley, Ted Selker. #GenerativeAI
• The secret of Ramsey numbers (A new order forms out of randomness). ~ Chris Edwards. #Math #CompSci
• Ética, pensamiento crítico y responsabilidad en el uso de la IA en trabajos académicos (presentación). ~ Lluís Codina. #GenerativeAI #Education

The readings shared in Mastodon on 30 October 2024 are

• Readings shared October 29, 2024. #AI #XAI #LLMs #Logic #Reasoning #ASP #LogicProgramming
• Lean 4 tactic cheatsheet (October 29, 2024). ~ Floris van Doorn. #ITP #Lean4
• AI and Mathematics. ~ Terence Tao. #AI #Math #ITP #Lean4
• A formal characterization of discrete condensed objects. ~ Dagur Asgeirsson. #ITP #Lean4 #Math
• Minimal, maximal, least, and greatest elements w.r.t. restricted ordering (in Isabelle/HOL). ~ Martin Desharnais. #ITP #IsabelleHOL
• Programming with Math: The lambda calculus. #LambdaCalculus
• Prolog, Datalog, languages, resources, and beyond! #Prolog #ASP #LogicProgramming
• Combining logic with Large Language Models for automatic debugging and repair of ASP programs. ~ Ricardo Brancas, Vasco Manquinho, Ruben Martins. #ASP #LogicProgramming #LLMs

The readings shared in Mastodon on 29 October 2024 are

• Readings shared October 28, 2024. #ITP #Lean4 #Coq #Math #LLMs
• Tools are all you need. ~ Henry Kautz. #AI #LLMs #Logic #Reasoning
• Logic in the age of AI. ~ Yuri Gurevich. #Logic #AI
• Rigorous language models for trustworthy AI. ~ Yanhong A. Liu. #AI #LLMs #Logic #Reasoning
• Harnessing ASP and its extensions: Recent applications and role in Trustworthy AI. ~ Giuseppe Mazzotta, Francesco Ricca. #AI #ASP #LogicProgramming
• Advancements in xASP, an XAI system for Answer Set Programming. ~ Mario Alviano, Ly Ly Trieu, Tran Son, Marcello Balduccini. #ASP #XAI
• Logic-based explainability: Past, present & future. ~ Joao Marques-Silva. #XAI #Logic
• A case study on TSP: What to optimize and how? ~ Martin Gebser. #ASP #LogicProgramming
• Integrating reasoning systems for trustworthy AI (Proceedings of the 4th Workshop on Logic and Practice of Programming (LPOP)). ~ Anil Nerode, Yanhong A. Liu (eds.) #Logic #LogicProgramming #AI
• Combining LLM code generation with formal specifications and reactive program synthesis. ~ William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito. #LLMs
• Keynote presentation by Hal Abelson and Gerald Sussman at the fourteenth RacketCon: "Teaching people thinking: programming and powerful ideas" and "From computational thinking to computational action". #CompSci
• Introduction to Git and GitHub for Python developers. ~ Jim Anderson. #Git

The readings shared in Mastodon on 28 October 2024 are

• Readings shared October 27, 2024. #ITP #Coq #Haskell #OCaml #Math #SetTheory #ChatGPT
• Lean: First steps (12 - Odd & Even). ~ Tariq Rashid #ITP #Lean4 #Math
• Lean: First steps (13 - Disequality). ~ Tariq Rashid #ITP #Lean4 #Math
• Prime number theorem and more. ~ Alex Kontorovich et als. #ITP #LeanProver #Math
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov, Anton Podkopaev. #ITP #Coq #LLMs

The readings shared in Mastodon on 27 October 2024 are

• Readings shared October 26, 2024. #ILP #LogicProgramming #AI #MachineLearning
• Double auctions: Formalization and automated checkers. ~ Mohit Garg, N. Raja, Suneel Sarswat, Abhishek Kr Singh. #ITP #Coq #Haskell #OCaml
• Axiomatic set theory (Version of 26 October 2024). ~ Tom Leinster. #Math #SetTheory
• ChatGPT’s performance in university admissions tests in mathematics. ~ Angel Udias et als. #ChatGPT #Math