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

The readings shared in Mastodon on 26 October 2024 are

• Readings shared October 25, 2024. #ITP #LeanProver #IsabelleHOL #Math #Prolog #ASP #CLP #LogicProgramming #LLMs #GenerativeAI #Rust #Verification
• Neuro-symbolic agent with ASP for robust exception learning in text-based games. ~ Kinjal Basu. #ILP #LogicProgramming #AI #MachineLearning
• An AI learning hierarchy. ~ Peter J. Denning, Ted G. Lewis. #AI

The readings shared in Mastodon on 25 October 2024 are

• A formal characterization of discrete condensed objects. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• Formalization of differential privacy in Isabelle/HOL. ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• A formalization of Borel determinacy in Lean. ~ #ITP #LeanProver #Math
• Brownian motion in Isabelle/HOL. ~ Christian Pardillo Laursen, Simon Foster, Mark Post. #ITP #IsabelleHOL
• Teaching pure LP with Prolog and a fair search rule. ~ Manuel V. Hermenegildo, Jose F. Morales, Pedro Lopez-Garcia. #Prolog #LogicProgramming
• General game playing - Killer app for logic programming. ~ Michael Genesereth. #Prolog #LogicProgramming
• Teaching Prolog through grammars. ~ David S. Warren. #Prolog #LogicProgramming
• From logic programming to programming in Logica: A first-course in declarative data science & engineering. ~ Evgeny Skvortsov, Yilin Xia, Shawn Bowers & Bertram Ludäscher. #LogicProgramming #Logica
• Logica: language of Big Data. ~ Evgeny Skvortsov et als. #LogicProgramming #Logica
• Democratising access to logic programming: A Web application design tool for querying Prolog code. ~ Santiago Andrés Villarroel, Christian Nelson Gimenez, Jorge Pablo Rodríguez, Laura Andrea Cecchi. #Prolog #LogicProgramming
• Computational thinking with logic programming. ~ Gopal Gupta, Elmer Salazar, Joaquín Arias. #ASP #LogicProgramming
• Generative logic: Teaching Prolog as Generative AI in art and design. ~ Christian Jendreiko. #Prolog #LogicProgramming #GenerativeAI
• Controlled natural language models. ~ Jacinto A. Dávila Quintero. #LLMs #Prolog #LogicProgramming
• On teaching logic programming in the era of generative AI. ~ Paul Tarau. #Prolog #LogicProgramming #GenerativeAI
• Bringing logic programming to primary school: a teacher training course. ~ Laura Andrea Cecchi, Jorge Pablo Rodríguez. #Prolog #LogicProgramming #Education
• On teaching constraint-based modeling and algorithms for decision support in Prolog. ~ François Fages. #CLP #LogicProgramming
• Desarrollo de sistema de resolución de rompecabezas en ASP mediante el uso de LLM. ~ Pedro Pazos Curra. #ASP #LLMs
• Verifying the Rust Standard Library. ~ Rahul Kumar et als. #Rust #Verification

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