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

The readings shared in Mastodon on 11 October 2024 are

• Readings shared October 10, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #Math #HoTT #LLMs
• ImProver: Agent-based automated proof optimization. ~ Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck. #ITP #LeanProver #LLMs
• Combining Waterproof and Mathematical Components (Utilising Mathematical Components in Waterproof to teach linear algebra proving). ~ Dick Arends. #ITP #Coq #Waterproof #Math
• Take-aways from using Deduce in the classroom. ~ Jeremy Siek. #ITP #Deduce
• The elementary theory of the category of sets (in Isabelle/HOL). ~ James Baxter & Dustin Bryant. #ITP #IsabelleHOL #Math
• Automated geometric theorem proving: Wu's method. ~ Joran Elias. #ATP #Math
• Can logic programming be liberated from predicates and backtracking? ~ Michael Hanus. #LogicProgramming

The readings shared in Mastodon on 10 October 2024 are

• Readings shared October 9, 2024. #Haskell #FunctionalProgramming
• #Exercitium: Número de ocurrencias de elementos. #Haskell
• M2Lyon2425: Group theory in Lean. ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #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 #Lean4 #Math
• Pointwise order of generalized Hofstadter functions G, H and beyond. ~ Pierre Letouzey, Shuo Li, Wolfgang Steiner. #ITP #Coq #Math
• Finite element method. Detailed proofs to be formalized in Coq. ~ François Clément, Vincent Martin. #ITP #Coq #Math
• Modelling and proving the monotonicity of processor pipelines in Coq. ~ Alban Gruin, Armelle Bonenfant, Thomas Carle, Christine Rochange. #ITP #Coq
• The Karatsuba square root algorithm (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Polynomial universes and dependent types. ~ C.B. Aberlé, David I. Spivak. #ITP #Agda
• Formalization of homotopy pushouts in homotopy type theory. ~ Vojtěch Štěpančík. #ITP #Agda #Math #HoTT
• AlphaIntegrator: Transformer action search for symbolic integration proofs. ~ Mert Ünsal, Timon Gehr, Martin Vechev. #LLMs #Math
• Demostraciones por inducción en Lean. ~ Luis Turcio. #ITP #Lean4

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, Andres Löh. #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. #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. #ITP #Agda #Logic #Math #CompSci
• PCC116: Lógica aplicada à computação (2024). ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #CompSci
• PCC116: Aula 1: Lógica proposicional em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math
• PCC116: Aula 2: Predicate logic in Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math
• PCC116: Aula 3: Programação funcional em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 4: Programação funcional e recursividade em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 5: Listas encadeadas (tipo List na biblioteca) em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 6: Predicados indutivos em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 8: Programando com tipos dependentes em Lean. ~ Rodrigo Ribeiro. #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