The readings shared in Mastodon on 9 October 2024 are

• Readings shared October 8, 2024. #ITP #IsabelleHOL #Lean4 #Mizar #Math #CompSci #Haskell #FunctionalProgramming #Emacs #OrgMode
• 18 months of the Haskell Unfolder. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming

The readings shared in Mastodon on 8 October 2024 are

• Readings shared October 7, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Calculemus #LLMs
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner, Detlef Plump. #ITP #IsabelleHOL
• Formal BOOK (formalizing "Proofs from THE BOOK" by Martin Aigner and Günter M. Ziegler). ~ Moritz Firsching, Nick Kuhn, Ralf Stephan, Christopher Schmidt. #ITP #Lean4 #Math
• Bonn Lean Course WiSe 24/25. ~ Floris van Doorn. #ITP #Lean4
• BonnLeanCourse: 1 - Introduction to Lean 4. ~ Floris van Doorn. #ITP #Lean4
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk, Cezary Kaliszyk. #ITP #Mizar #Math
• What is theoretical computer science? ~ Moshe Y. Vardi. #CompSci #Math
• Literate Org Haskell. ~ F. Murillo. #Emacs #OrgMode #Haskell #FunctionalProgramming
• Using Org Mode to write and organize a book. ~ Ron Galloway. #Emacs #OrgMode

The readings shared in Mastodon on 7 October 2024 are

• Readings shared October 6, 2024. #ITP #LeanProver #Logic #Math #AI #Python
• Proofs of the pigeonhole principle in Lean4. #ITP #Lean4 #Math #Calculemus
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Repo for the first BerLean workshop. #ITP #Lean4 #Math
• Re-invention of group/ring algebra in Lean 4 for learning purposes. ~ Eugene Zolotarev. #ITP #Lean4 #Math
• Introduction to mathematical arguments (background handout for courses requiring proofs). ~ Michael Hutchings. #Logic #Math
• How to write proofs: a quick guide. ~ Eugenia Cheng. #Logic #Math
• Notes on math proof. ~ Bruce Ikenaga. #Logic #Math
• Proof writing and presentation tips. ~ Erika L.C. King. #Logic #Math
• How to write mathematics. ~ Martin Erickson. #Logic #Math
• Advice on mathematical writing. ~ Keith Conrad. #Math
• Examples of proofs by induction. ~ Keith Conrad. #Math
• An introduction to proofs and the mathematical vernacular. ~ Martin V. Day. #Math
• Conventions for writing mathematical proofs. ~ John M. Lee. #Math
• TheoremLlama: Transforming general-purpose LLMs into Lean4 experts. ~ Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang. #ITP #Lean4 #LLMs

The readings shared in Mastodon on 6 October 2024 are

• Readings shared October 5, 2024. #ITP #LeanProver #Lean4 #Agda #Logic #Math #FunctionalProgramming #AI
• Grelling–Nelson paradox. #Logic
• Formalization of the Grelling's paradox in the Lean theorem prover. ~ Juan Pablo Yamamoto (@jpyamamoto@mathstodon.xyz). #ITP #LeanProver #Logic
• Proofs shown to be wrong after formalization with proof assistant. #ITP #Math
• We're entering uncharted territory for Math (Terence Tao, the world’s greatest living mathematician, has a vision for AI). ~ Matteo Wong. #Math #AI #ITP
• Curso Python para Matemáticas. ~ Javier García-Algarra. #Matemáticas #Python

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