The readings shared in Mastodon on 5 October 2024 are

• Readings shared October 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Python
• ENS-Lean-course: Taxicab number in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Sets in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Homework 3: Sets. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• PCC116-2021: Lógica aplicada à computação (2021/22). ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Agda #Logic #Math #CompSci
• PCC116: Lógica aplicada à computação (2024). ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #CompSci
• PCC116: Aula 1: Lógica proposicional em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math
• PCC116: Aula 2: Predicate logic in Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math
• PCC116: Aula 3: Programação funcional em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 4: Programação funcional e recursividade em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 5: Listas encadeadas (tipo List na biblioteca) em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 6: Predicados indutivos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 8: Programando com tipos dependentes em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 9: Sobrecarga e classes de tipos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 10: Metaprogramação e automação de provas em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 11: Recursão geral em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 12: Representando semântica formal em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 13: λ-cálculo tipado simples em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 14: Formalizando em Lean compiladores / semântica de linguagens imperativas. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 15: Modelagem de autômatos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• Terence Tao’s vision of AI assistants in research mathematics. ~ David H Bailey. #Math #AI #ITP #LeanProver

The readings shared in Mastodon on 4 October 2024 are

• Readings shared October 3, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Proofs of "If f ∘ f is bijective, then f is bijective" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Abstract substitution (in Isabelle/HOL). ~ Martin Desharnais. #ITP #IsabelleHOL
• Discrete Math. ~ Mohamed Jamaloodeen, Kathy Pinzon, Daniel Pragel, Joshua Roberts & Sebastien Siva. #Math #Python

The readings shared in Mastodon on 1 October 2024 are

• Readings shared September 30, 2024. #ITP #LeanProver #Lean4 #Math #LambdaCalculus
• ENS-Lean_course: Homework 2 (Logic). ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• The geometry game. ~ Marc Masdeu. (@marcmasdeu). #ITP #Lean3 #Math
• Parallel shear sort (in Isabelle/HOL). ~ Manuel Eberl & Peter Lammich. #ITP #IsabelleHOL #Algorithms
• Rule synthesis etudes for Tao's algebra problem. ~ Philip Zucker (@SandMouth). #ATP #SMT #Z3
• Functional programming course for Telecom Nancy, using Haskell. ~ Clément Hurlin (@smelc3). #Haskell #FunctionalProgramming
• Integrando AI con mi herramienta de trabajo preferida: Google Gemini, Emacs Lisp y GNU/Linux!! ~ lksadj. #Emacs #AI #GoogleGemini

The readings shared in Mastodon on 30 September 2024 are

• Readings shared September 29, 2024. #ITP #LeanProver #Lean4 #Logic #Math #Haskell #FunctionalProgramming #Prolog #ASP #LogicProgramming #AI
• Introduction to the λ-calculus. ~ Lawrence C. Paulson (@LawrPaulson@mathstodon.xyz). #LambdaCalculus
• How to read Lean. ~ Martin Dvořák. #ITP #LeanProver #Math
• Certifying rings of integers in number fields. ~ Anne Baanen, Alain Chavarri Villarello & Sander R. Dahmen. #ITP #Lean4 #Math

The readings shared in Mastodon on 29 September 2024 are

• Readings shared September 28, 2024. #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math
• M2Lyon2425: Sets and functions (Solutions). ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• M2Lyon2425: Sets and functions. ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Introduction to Lean. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Proofs by calculation. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Using theorems in Lean. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Lean style guidelines. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Homework 1 (Sep 21, 2024). ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Logic in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• Con(NF): A formal consistency proof of Quine's set theory New Foundations. ~ Sky Wilshaw et als. #ITP #Lean4 #Math
• Welcome to the parti(tioning) (Functional Pearl): Using rewrite rules and specialisation to partition Haskell programs. ~ Robert Krook & Samuel Hammersber. #Haskell #FunctionalProgramming
• The Marseille-Edinburgh connection. ~ Robert Kowalski. #Prolog #LogicProgramming
• PROLOG en son temps: hier, aujourd’hui, demain. Un point de vue industriel, économique et géopolitique. ~ Jean Rohmer. #Prolog #LogicProgramming
• L’IA symbolique et le dépassement de la logique classique. ~ Henri Prade. #AI #Logic #Prolog #LogicProgramming
• ASP: un devenir de Prolog. ~ Belaïd Benhamou, Vincent Risch & Éric Würbel. #LogicProgramming #Prolog #ASP
• Dimensions linguistiques de Prolog : le passé, le futur. ~ Verónica Dahl. #Prolog #AI

The readings shared in Mastodon on 28 September 28 2024 are

• Readings shared September 27, 2024. #ATP #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Math #CategoryTheory #SetTheory
• Hyperstability in the Erdős-Sós conjecture. ~ Alexey Pokrovskiy. #ITP #LeanProver #Math
• Formalized soundness and completeness of epistemic logic. ~ Asta Halkjær From, Alexander Birch Jensen & Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Math
• Löb’s theorem and provability predicates in Coq. ~ Janis Bailitis. #ITP #Coq #Logic #Math
• Formalizing potential flows using the HOL Light theorem prover. ~ Elif Deniz & Sofiène Tahar. #ITP #HOL_Light
• Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid & Sofiène Tahar. #ITP #HOL_Light

The readings shared in Mastodon on September 27, 2024 are

• A pilot project in universal algebra to explore new ways to collaborate and use machine assistance? ~ Terence Tao (@tao@mathstodon.xyz). #ITP #LeanProver #Lean4 #Math
• Equational theory project. ~ Terence Tao et als. #ITP #ATP #Math
• Equational theories (Blueprint). ~ Terence Tao (@tao@mathstodon.xyz). #ITP #Lean4 #Math
• Knuckledragger solvers for Terence Tao's equational reasoning challenge. ~ Philip Zucker (@SandMouth). #ITP #Math
• Linear algebra in "Mathematics in Lean". ~ Patrick Massot. #ITP #Lean4 #Math
• Lean: First steps (09 - "Or" goal). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #Lean4 #Math
• Lean: First steps (11 - Existence). ~ Tariq Rashid (@rzeta0@mastodon.social) #ITP #Lean4 #Math
• Post’s problem and the priority method in synthetic computability. ~ Haoyi Zeng. #ITP #Coq
• Secure smart contracts with Isabelle/Solidity. ~ Diego Marmsoler, Asad Ahmed & Achim D. Brucker. #ITP #IsabelleHOL
• Theoretical and practical approach to the soundness and completeness of operational semantics based on denotational semantics for MDESL. ~ Hongyan Zhao, Huibiao Zhu, Feng Sheng, Jifeng He & Jonathan Bowen. #ITP #Coq
• The universal presence of category theory. ~ Gabriel Field. #Math #CategoryTheory
• Axiomatic set theory (Version of 24 September 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on September 25, 2024 are

• Readings shared September 24, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #SetTheory #Haskell #FunctionalProgramming #AI #LLMs
• Proofs of the Brahmagupta-Fibonacci identity in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• M2Lyon2425: Sets and functions (1). ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• Cambridge combinatorics in Lean (Formalisation of the Cambridge combinatorics courses). ~ Yaël Dillies. #ITP #LeanProver #Lean4 #Math
• The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. #ITP #LeanProver #Lean4 #Mathlib #Math
• Math-Haskell Rosetta Stone - Part 1. ~ Daniel Brice (@friedbrice_). #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 24, 2024 are

• Readings shared September 23, 2024. #ITP #LeanProver #Coq #IsabelleHOL #Math #ITP #Haskell #FunctionalProgramming #AI #LLMs
• Proofs of ∑k<n. 2ᵏ = 2ⁿ-1 in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Code examples from a Lean tutorial at the Copenhagen functional programming meetup (1/2). ~ David Thrane Christiansen (@d_christiansen@mathstodon.xyz). #ITP #Lean4 #FunctionalProgramming
• Code examples from a Lean tutorial at the Copenhagen functional programming meetup (2/2). ~ David Thrane Christiansen (@d_christiansen@mathstodon.xyz). #ITP #Lean4 #FunctionalProgramming
• Playing with a game. ~ Chris Smith. #Haskell #FunctionalProgramming
• Applicative logic. ~ Håkon Robbestad Gylterud. #Haskell #FunctionalProgramming #Logic
• Axiomatic set theory 1: Introduction. ~ Tom Leinster. #Math #SetTheory
• Axiomatic set theory (Version of 21 September 2024). ~ Tom Leinster. #Math #SetTheory
• On logic and generative AI. ~ Yuri Gurevich, Andreas Blass. #Logic #AI
• Proof automation with Large Language Models. ~ Minghai Lu, Benjamin Delaware, Tianyi Zhang. #ITP #Coq #LLMs
• ChatGPT as a solver and grader of programming exams written in spanish. ~ Pablo Fernández-Saborido, Marcos Fernández-Pichel, David E. Losada. #LLMs #ChatGPT #CompSci
• Is math the path to chatbots that don't make stuff up? ~ Cade Metz. #AI #ITP #Lean4 #Math
• Harmonic: We are forging the world's most advanced mathematical reasoning engine. #AI #ITP #Math

The readings shared in Mastodon on September 23, 2024 are

• Readings shared September 22, 2024. #ITP #LeanProver #Lean3 #Lean4 #Logic #Math
• Introduction to Lean. ~ Markus Himmel. #ITP #LeanProver #Math
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #LeanProver #Math
• Tips and tricks for beginners using Mathlib/Lean. ~ Moritz Firsching. #ITP #LeanProver
• Lean Tutorial in Vienna. ~ Pietro Monticone et als. #ITP #LeanProver #Math
• Turning the Coq proof assistant into a pocket calculator. ~ Guillaume Melquiond. #ITP #Coq
• A case for first-class environments. ~ Jinhao Tan & Bruno C. D. S. Oliveira. #ITP #Coq
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #AI #LLMs
• Rabin's closest pair of points algorithm (in Isabelle/HOL). ~ Emin Karayel & Zixuan Fan. #ITP #IsabelleHOL
• Wlog – Without loss of generality (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL
• Haskell tutorial and cookbook. ~ Mark Watson. #Haskell #FunctionalProgramming