The readings shared in Mastodon on 17 October 2024 are

• Readings shared October 16, 2024. #AI #Education #FunctionalProgramming #Haskell #ITP #Lean4 #MachineLearning #Math1
• The Haskell Unfolder Episode 34: You already understand monads. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Ollama-haskell: Haskell bindings for Ollama. ~ Tushar Adhatrao. #Haskell #FunctionalProgramming #Ollama #LLMs
• Big advance on simple-sounding math problem was a century in the making. ~ Erica Klarreich. #Math
• Thinking about 12 aspects of personal information/knowledge management. ~ Sacha Chua. #Emacs #OrgMode
• Manual en español de GNU/Emacs 29.1. ~ Tano. #Emacs

The readings shared in Mastodon on 16 October 2024 are

• Readings shared October 15, 2024. #AI #ChatGPT #Emacs #FunctionalProgramming #GeoGebra #Haskell #ITP #LambdaCalculus #Lean4 #LeanProver #LogicProgramming #Math #OrgMode #Prolog
• Lean: First steps (13 - Disquality). ~ Tariq Rashid #ITP #Lean4 #Math
• Munihac WASM experiment: convert Haskell expressions to pointfree in your browser. ~ Sergey Vinokurov. #Haskell #FunctionalProgramming
• Por qué debemos enseñar Machine Learning en todos los títulos universitarios. ~ Manuel de León Rodríguez y Rodrigo Trujillo González. #Education #AI #MachineLearning

The readings shared in Mastodon on 15 October 2024 are

• Readings shared October 13, 2024. #AI #CategoryTheory #Coq #Education #FunctionalProgramming #Haskell #ITP #ITP
• On using GeoGebra and ChatGPT for geometric discovery. ~ Francisco Botana, Tomás Recio, María Pilar Vélez. #GeoGebra #ChatGPT #Math #AI
• Lean: First steps (12 - Odd & Even ). ~ Tariq Rashid #ITP #Lean4 #Math
• Tutorial videos for the course "Lean: First Steps". ~ Tariq Rashid. #ITP #Lean4 #Math
• The handshaking lemma. ~ Christoph Spiegel. #ITP #LeanProver #Lean4 #Math
• Water sort in Haskell. ~ Nicolas Audinet de Pieuchon. #Haskell #FunctionalProgramming
• The power of Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Programación lógica con restricciones. #Prolog #LogicProgramming
• Emacs para ciencias del dato. #Emacs #OrgMode
• The λ-calculus, 2: The Church-Rosser theorem. ~ Lawrence Paulson. #LambdaCalculus

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

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.. #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. #ATP #SMT #Z3
• Functional programming course for Telecom Nancy, using Haskell. ~ Clément Hurlin. #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. #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. #ITP #LeanProver #Lean4 #Math
• Equational theory project. ~ Terence Tao et als. #ITP #ATP #Math
• Equational theories (Blueprint). ~ Terence Tao. #ITP #Lean4 #Math
• Knuckledragger solvers for Terence Tao's equational reasoning challenge. ~ Philip Zucker. #ITP #Math
• Linear algebra in "Mathematics in Lean". ~ Patrick Massot. #ITP #Lean4 #Math
• Lean: First steps (09 - "Or" goal). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (11 - Existence). ~ Tariq Rashid #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. #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. #ITP #Lean4 #FunctionalProgramming
• Code examples from a Lean tutorial at the Copenhagen functional programming meetup (2/2). ~ David Thrane Christiansen. #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

The readings shared in Mastodon on September 22, 2024 are

• Readings shared September 21, 2024. #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning
• Lean: First steps (08 - "And" hypothesis). ~ Tariq Rashid. #ITP #Lean4 #Math
• Using Lean theorem prover to teach formal mathematics: Lean-Intro-Topology library. ~ Rafael Grenier. #ITP #LeanProver #Lean4 #Math
• Lean-Intro-Topology: Introduction to topology with Lean. ~ Rafael Grenier. #ITP #LeanProver #Lean4 #Math
• "A concise introduction to mathematical logic" in Lean4. ~ Enrico Borba. #ITP #LeanProver #Lean4 #Logic #Math
• Lean proofs of (some) problems from the book "102 combinatorial problems". ~ Musab Guma'a et als. #ITP #LeanProver #Lean4 #Math
• The Topology Game (Learn topology with Lean!). ~ Barcelona Lean Seminar. #ITP #LeanProver #Math
• Source of the "The Topology Game". ~ Marc Masdeu et als. #ITP #LeanProver #Lean3 #Math
• Formalization of Riemann-Stieltjes integral in Lean4. ~ Marc Masdeu et als. #ITP #LeanProver #Lean4 #Math
• A Lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms. ~ Mattchen. #ITP #LeanProver #Lean4 #Math
• Formalisation of mathematics and dependent-type programming (A tutorial introduction using the Lean4 theorem prover). ~ Frédéric Peschanski. #ITP #LeanProver #Lean4 #Math
• A tutorial introduction of dependently-typed programming (and the Lean4 theorem prover). ~ Frédéric Peschanski. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on September 21, 2024 are

• Readings shared September 20, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4
• Course: Theorem proving with Lean. ~ Damiano Testa. #ITP #LeanProver #Math
• Finding lemmas in Mathlib. ~ Damiano Testa. #ITP #LeanProver #Mathlib
• Course: Repository for the Lean master program in Lyon for 2024-25. ~ Filippo A. E. Nuccio et als. #ITP #LeanProver #Math
• Weekly-Lean: The Lean weekly challenge. ~ Kyle Thompson, Saketh Kasibatla & Nico Lehmann. #ITP #LeanProver
• Mini-curso de Lean. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Lean - Tácticas y proposiciones. ~ Luis Turcio. #ITP #LeanProver
• Lean - Proposiciones y primer orden. ~ Luis Turcio. #ITP #LeanProver #Logic
• Lean - Conjuntos 1. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Lean - Funciones. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Topología general en Lean3. ~ Miguel Marco. #ITP #LeanProver #Lean3 #Math
• Juego LEAN de topología general. ~ Miguel Marco. #ITP #LeanProver #Lean4 #Math
• Stone duality in Lean. ~ Dagur Ásgeirsson, Sam van Gool, Tomáš Jakl & Filippo A.E. Nuccio. #ITP #LeanProver #Lean4 #Math
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving. ~ Kangfeng Ye, Jim Woodcock & Simon Foster. #ITP #IsabelleHOL
• No generalization without understanding and explanation (Why AI needs symbolic and logical reasoning). ~ Walid Saba. #AI #LLMs #DeepLearning #Logic
• Qwen2.5-Math: The world's leading open-sourced mathematical LLMs. #LLMs #Math
• Qwen2.5-Coder Technical Report. ~ Binyuan Hui et als. #LLMs #Programming

The readings shared in Mastodon on September 20, 2024 are

• Readings shared September 19, 2024. #ITP #Coq #Math #Haskell #FunctionalProgramming #Logic #AI
• Proofs of "∑i<n. i = n(n-1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #CaWlculemus
• Extending Isabelle/HOL's code generator with support for the Go programming language. ~ Terru Stübinger & Lars Hupel. #ITP #IsabelleHOL #GoLang
• Mapping probability with logic: First order models in puzzle solving. ~ Adrian Groza. #ATP #Prover9 #Mace4

The readings shared in Mastodon on September 19, 2024 are

• Readings shared September 18, 2024. #ITP #IsabelleHOL
• An imperative language for verified exact real-number computation. ~ Andrej Bauer, Sewon Park & Alex Simpson. #ITP #Coq #Math
• The Haskell Unfolder Episode 32: Solving tic-tac-toe. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What is logic-based/logicist AI? (Its history). ~ Selmer Bringsjord. #Logic #AI
• The failure of Deep Learning (GPT-4o bites the dust). ~ Selmer Bringsjord. #Logic #AI
• AI should challenge, not obey (Let’s transform our robot secretaries into Socratic gadflies). ~ Advait Sarkar. #AI #CriticalThinking
• La mecánica cuántica explicada de otra forma fácil de entender y en su contexto histórico. ~ @Alvy. #Física

The readings shared in Mastodon on September 18, 2024 are

• Readings shared September 17, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Autoformalization #Emacs
• Combining classical and probabilistic independence reasoning to verify the security of oblivious algorithms. #ITP #IsabelleHOL
• Efficient formally verified maximal end component decomposition for MDPs. ~ Arnd Hartmanns, Bram Kohlen & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on September 17, 2024 are

• Readings shared September 16, 2024. #ITP #LeanProver #Lean4 #Math #Haskell #FunctionalProgramming
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #LeanProver #Lean4 #Math
• Towards verified polynomial factorisation. ~ James H. Davenport. #ITP #LeanProver #Math
• First steps towards computational polynomials in Lean. ~ James H. Davenport. #ITP #LeanProver #Math
• miniCodeProps: A minimal benchmark for proving properties of code. ~ Evan Lohn & Sean Welleck. #ITP #LeanProver #Lean4 #LLMs
• Leveraging large language models for autoformalizing theorems: A case study. ~ Michail Karatarakis. #ITP #LeanProver #Lean4 #Autoformalization #Math
• Concrete bounds for Chebyshev’s prime counting functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Why Emacs is the best: 10 key advantages. ~ Tristan de Cacqueray. #Emacs

The readings shared in Mastodon on September 16, 2024 are

• Readings shared September 15, 2024. #ITP #LeanProver #Lean4 #LLMs
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak & Vladimir Kolmogorov. #ITP #LeanProver #Lean4 #Math
• The Haskell playground. ~ Tom Smeding. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 15, 2024 are

• Readings shared September 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs
• LLMlean integrates LLMs and Lean for tactic suggestions, proof completion, and more. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs
• LeanDojo: Theorem Proving in Lean using Language Models. ~ Kaiyu Yang et als. #ITP #LeanProver #Lean4 #LLMs
• llmstep: [L]LM proofstep suggestions in Lean 4. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs

The readings shared in Mastodon on September 14, 2024 are

• Readings shared September 13, 2024. #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode
• AI for Mathematics: Mathematical formalized problem solving and theorem proving in different fields in Lean 4. ~ Xichen Tang. #ITP #LeanProver #Lean4 #Math
• Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. #ITP #HOL_Light
• A simple proof that π is irrational (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Decidable equality for indexed data types. ~ Brent Yorgey. #ITP #Agda #FunctionalProgramming
• Why Haskell? ~ Gideon Farrell. #Haskell #FunctionalProgramming
• Type-theoretic considerations in functional language software development. ~ David Michael Roberts. #Haskell #FunctionalProgramming #ITP #IsabelleHOL
• Simulation of lambda terms in lambda calculus. ~ Helmut Brandl. #LambdaCalculus
• Estrenando el nuevo modelo de OpenAI: o1-preview. Resolviendo con ChatGPT un problema de Matemáticas II de la Prueba de Acceso a la Universidad EBAU. ~ Luis M. Iglesias. #LLMs #Matemáticas

The readings shared in Mastodon on September 13, 2024 are

• Readings shared September 12, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. #Haskell #FunctionalProgramming #LiquidHaskell
• Why and how I use "Org Mode" for my writing and more. ~ Aditya Athalye. #Emacs #OrgMode

The readings shared in Mastodon on September 12, 2024 are

• Readings shared September 11, 2024. #ITP #IsabelleHOL #LeanProver #Coq #NaprocheZF #Natty #AlphaGeometry #AlphaProof #FunctionalProgramming #OCaml #Logic #Math #IMO #AI #MachineLearning #LLMs
• Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• The undecidability of contextual equivalence on PCF2 (Towards a mechanisation in Coq). ~ Fabian Andreas Brenner. #ITP #Coq
• 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 September 11, 2024 are

• Readings shared September 10, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #Python #Math
• Mathematical Olympiad (To the geometry and beyond…). ~ Mirek Olšák. #Math #ITP #AI #IMO #AlphaGeometry #AlphaProof #LeanProver
• Isabelle/RL project proposal: Reinforcement learning on the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #MachineLearning
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #LLMs
• ATPs as universal AIs: What do AGI architectures suggest for ATP research? ~ Zarathustra Goertzel. #ATP #AI
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq
• The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? ~ Jason Rute. #ITP #AI #LLMs
• Naproche-ZF: Lessons learned from implementing a new natural-language-oriented theorem prover. ~ Adrian De Lon. #ITP #NaprocheZF #Math
• Natural-language proof assistant for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math #OCaml
• A few open problems in neural theorem proving (in Lean). ~ Sean Welleck. #ITP #LeanProver #LLMs
• Project description: Experiments with language models for Isabelle autoformalization. ~ David Valente, Manuel Eberl, Cezary Kaliszyk & Josef Urban. #ITP #IsabelleHOL #Autoformalization
• Provably safe systems: Prospects and approaches. ~ Mario Carneiro. #ITP #AI
• With fifth busy beaver, researchers approach computation’s limits. ~ Ben Brubaker. #ITP #Coq #Math #CompSci
• Kids should be taught to think logically. ~ Vinay K. Chaudhri. #Logic

The readings shared in Mastodon on September 10, 2024 are

• Readings shared September 9, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming #Python
• Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)² in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• #Exercitium: Sumas de dos abundantes. #Haskell #Python #Matemáticas
• Types as interfaces. ~ Chris. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 9, 2024 are

• Readings shared September 8, 2024. #ITP #Agda #Math #Haskell #FunctionalProgramming
• Proofs of "a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing a knight's tour with Prolog. ~ Markus Triska. #Prolog #FunctionalProgramming
• String Knuth Bendix. ~ Philip Zucker. #Math #Python

The readings shared in Mastodon on September 8, 2024 are

• Readings shared September 7, 2024. #ITP #Lean4 #IsabelleHOL #Maude #ATP #Prover9 #Math #Calculemus
• Formalization of the structure sheaf of a ring spectrum. ~ Maša Žaucer. #ITP #Agda #Math
• Automatic test-case generation for Haskell based on dependent types. ~ Pablo Castellanos García. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 7, 2024 are

• Readings shared September 6, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning
• Proofs of "a+(a+d)+(a+2d)+···+(a+nd) = (n+1)(2a+nd)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Metaprogramming in Lean. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Examples using MetaProgramming for writing tactics. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Formalisation of Hall’s theorem for countable infinite graphs. ~ Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón & Thaynara Arielly de Lima. #ITP #IsabelleHOL #Math
• First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. #ATP #Prover9 #Math
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #Maude #LeanProver #Lean3

The readings shared in Mastodon on September 6, 2024 are

• Readings shared September 5, 2024. #ITP #LeanProver #Lean4 #IsabelleHO #Agda #Logic #Math #Calculemus #Haskell #OCaml #FunctionalProgramming #AI
• Towards solid abelian groups: A formal proof of Nöbeling’s theorem. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• The directed Van Kampen theorem in Lean. ~ Henning Basold, Peter Bruin & Dominique Lawson. #ITP #LeanProver #Lean4 #Math
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens & Tobias Grosser. #ITP #LeanProver
• Duper: A proof-producing superposition theorem prover for dependent type theory. ~ Joshua Clune, Yicheng Qian, Alexander Bentkamp & Jeremy Avigad. #ITP #LeanProver #Lean4
• Teaching mathematics using Lean and controlled natural language. ~ Patrick Massot. #ITP #LeanProver #Lean4 #Math
• Lean formalization of completeness proof for Coalition Logic with Common Knowledge. ~ Kai Obendrauf, Anne Baanen, Patrick Koopmann & Vera Stebletsova. #ITP #LeanProver #Lean4
• Formal verification of the empty hexagon number. ~ Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro & Marijn J. H. Heule. #ITP #LeanProver #Lean4
• Integrals within integrals: A formalization of the Gagliardo-Nirenberg-Sobolev inequality. ~ Floris van Doorn & Heather Macbeth. #ITP #LeanProver #Lean4 #Math
• Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4. ~ Sam Ezeh. #ITP #LeanProver #Lean4 #Math
• Formalising half of a graduate textbook on number theory. ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson & Wenda Li. #ITP #IsabelleHOL #Math
• A formalization of the Lévy-Prokhorov metric in Isabelle/HOL. ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• Alpha-beta pruning verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• A formal analysis of capacity scaling algorithms for minimum cost flows. ~ Mohammad Abdulaziz & Thomas Ammer. #ITP #IsabelleHOL
• An operational semantics in Isabelle/HOL-CSP. ~ Benoît Ballenghien & Burkhart Wolff. #ITP #IsabelleHOL
• A verified earley parser. ~ Martin Rau & Tobias Nipkow. #ITP #IsabelleHOL
• A modular formalization of superposition in Isabelle/HOL. ~ Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette & Sophie Tourret. #ITP #IsabelleHOL
• Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. #ITP #IsabelleHOL
• A generalised union of rely–guarantee and separation logic using permission algebras. ~ Vincent Jackson, Toby Murray & Christine Rizkallah. #ITP #IsabelleHOL
• An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility. ~ Dohan Kim. #ITP #IsabelleHOL
• A Coq formalization of Taylor models and power series for solving ordinary differential equations. ~ Sewon Park & Holger Thies. #ITP #Coq #Math
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt & Zachary Stone. #ITP #Coq #Math
• Taming differentiable logics with Coq formalisation. ~ Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz & Kathrin Stark. #ITP #Coq #Logic #MachineLearning
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici & Nobuko Yoshida. #ITP #Coq
• End-to-end formal verification of a fast and accurate floating-point approximation. ~ Florian Faissole, Paul Geneau de Lamarlière & Guillaume Melquiond. #ITP #Coq
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue & Takafumi Saikawa. #ITP #Coq
• Verifying software emulation of an unsupported hardware instruction. ~ Samuel Gruetter, Thomas Bourgeat & Adam Chlipala. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq
• Formalizing the algebraic small object argument in UniMath. ~ Dennis Hilhorst & Paige Randall North. #ITP #Coq #Math
• The Rewster: Type preserving rewrite rules for the Coq proof assistant. ~ Yann Leray, Gaëtan Gilbert, Nicolas Tabareau & Théo Winterhalter. #ITP #Coq
• Correctly compiling proofs about programs without proving compilers correct. ~ Audrey Seo, Christopher Lam, Dan Grossman & Talia Ringer. #ITP #Coq
• Redex2Coq: Towards a theory of decidability of redex’s reduction semantics. ~ Mallku Soldevila, Rodrigo Ribeiro & Beta Ziliani. #ITP #Coq
• Defining and preserving more C behaviors: Verified compilation using a concrete memory model. ~ Andrew Tolmach, Chris Chhak & Sean Anderson. #ITP #Coq
• Robust mean estimation by all means. ~ Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa & Carsten Schürmann. #ITP #Coq
• Abstractions for multi-sorted substitutions. ~ Hannes Saffrich. #ITP #Agda
• The functor of points approach to schemes in Cubical Agda. ~ Max Zeuner & Matthias Hutzler. #ITP #Agda
• A formalization of the general theory of quaternions. ~ Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro & Mauricio Ayala-Rincón. #ITP #PVS #Math
• Formalizing the Cholesky factorization theorem. ~ Carl Kwan & Warren A. Hunt Jr. #ITP #ACL2 #Math
• A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. #ITP #HOL4 #Math
• Mechanized HOL reasoning in set theory. ~ Simon Guilloud, Sankalp Gambhir, Andrea Gilot & Viktor Kunčak. #ITP #Lisa #Math
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk & Cezary Kaliszyk. #ITP #Mizar #Math
• 15th International Conference on Interactive Theorem Proving (ITP 2024,). #ITP
• The code of Mathematics: Proof and truth ~ Stefan Müller-Stach. #Math
• Neuro-symbolic theorem proving with Lean. ~ Peiyang Song. #ITP #LeanProver #AI #MachineLearning

The readings shared in Mastodon on September 5, 2024 are

• Readings shared September 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming
• Proofs of "0+1+2+3+···+n=n(n + 1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Lean: First steps (07 - Proof by cases). ~ Tariq Rashid. #ITP #Lean4 #Math
• Logic and proof. ~ Jeremy Avigad, Robert Y. Lewis & Floris van Doorn. #ITP #LeanProver #Lean4 #Logic #Math
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch & Axel Ljungström.3# #ITP #Agda
• Sized types and coinduction in Safe Agda. ~ Isaac Elliott. #Agda #FunctionalProgramming
• OCaml scientific computing. #OCaml #FunctionalProgramming #AI
• LSP: the good, the bad, and the ugly. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
• Parsers are relative bimonads. ~ Artemis. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 4, 2024 are

• Readings shared September 3, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Proofs of "If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Seven levels of type safety in Haskell: Lists. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 3, 2024 are

• Readings shared September 2, 2024. #ITP #Lean4 #LeanProver #IsabelleHOL #Coq #Maude #Math #Calculemus #FunctionalProgramming
• Proofs of "If x is the limit of u and y is an upper bound of u, then x ≤ y" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• An exponential improvement for diagonal Ramsey (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Extension of stateful intransitive noninterference with inputs, outputs, and nondeterminism in language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
• Definitive set semantics for LTL3 (in Isabelle/HOL). ~ Rayhana Amjad, Rob van Glabbeek & Liam O’Connor. #ITP #IsabelleHOL

The readings shared in Mastodon on September 2, 2024 are

• Readings shared September 1, 2024. #ITP #Agda
• Proofs of "If (∀ ε > 0, y ≤ x + ε), then y ≤ x" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #LeanProver #Maude
• Scaling the evolution of verified software. ~ Kiran Gopinathan. #PhDThesis #ITP #Coq
• Ramsey number bounds (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Lean 4.11.0. ~ David Thrane Christiansen. #ITP #Lean4 #FunctionalProgramming

The readings shared in Mastodon on September 1, 2024 are

• Readings shared August 31, 2024. #ITP #Lean4 #IsabelleHOL #Theorema #Coq #Agda #Math #HoTT #Calculemus #PhDThesis
• Modal μ-calculus for free in Agda. ~ Ivan Todorov & Casper Bach Poulsen. #ITP #Agda

The readings shared in Mastodon on August 31, 2024 are

• Readings shared August 30, 2024. #ITP #IsabelleHOL #Agda #Logic #Math #Nix #Haskell #FunctionalProgramming #LogicProgramming
• Proofs of "If x is the supremum of set A, then (∀ y, y < x → ∃ a ∈ A, y < a) in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Unifying model execution and deductive verification with interaction trees in Isabelle/HOL. ~ Simon Foster, Chung-Kil Hur & Jim Woodcock.7# #ITP #IsabelleHOL
• Certification of sorting algorithms using Theorema and Coq. ~ Isabela Drămnesc, Tudor Jebelean & Sorin Stratulat. #ITP #Theorema #Coq
• Investigations in graph-theoretical constructions in Homotopy Type Theory. ~ Jonathan Prieto-Cubides. #PhDThesis #ITP #Agda #HoTT

The readings shared in Mastodon on August 30, 2024 are

• Readings shared August 29, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #Calculemus
• Compactness theorem for propositional logic and combinatorial applications. ~ Fabián Fernando Serran Suárez, Thaynara Arielly de Lima & Mauricio Ayala-Rincón. #ITP #IsabelleHOL #Logic #Math
• Law and order for typestate with borrowing. ~ Hannes Saffrich, Yuki Nishida & Peter Thiemann.1# #ITP #Agda
• Getting started with Nix for Haskell. ~ Abhinav Sarkar. #Nix #Haskell #FunctionalProgramming
• Logic programming with extensible types. ~ Ivan Perez & Angel Herranz. #Haskell #FunctionalProgramming #LogicProgramming

The readings shared in Mastodon on August 29, 2024 are

• Readings shared August 28, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Math #Calculemus #AI
• Proofs of the equivalence of two definitions of the Fibonacci function in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A residual service curve computable in quadratic time for network calculus. ~ Marc Boyer & Pierre Roux. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq

The readings shared in Mastodon on August 28, 2024 are

• Readings shared August 27, 2024. #ITP #IsabelleHOL #Math
• Proofs of "flatten (mirror a) = reverse (flatten a)" in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Formalizing Mason-Stothers theorem and its corollaries in Lean 4. ~ Jineon Baek & Seewoo Lee. #ITP #LeanProver #Lean4 #Math
• On the maximum weighted irredundant set problem. ~ Ricardo D. Katz & Daniel Severín. #ITP #Coq #Math
• Compositional verification of composite byzantine protocols. ~ Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey. #ITP #Coq
• The top 100 gen AI consumer apps. ~ Olivia Moore. #AI
• Conocimientos de sentido común: el obstáculo de la IA en el camino hacia la inteligencia artificial general. ~ Ramón López de Mántaras. #IA
• Las herramientas de IA que están captando la atención de la gente. ~ @Alvy #IA
• L’intelligence artificielle : Hier, aujourd’hui … et demain. ~ Jean-Paul Haton. #AI

The readings shared in Mastodon on August 27, 2024 are

• Readings shared August 26, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming
• Topological groups (in Isabelle/HOL). ~ Niklas Krofta. #ITP #IsabelleHOL #Math
• Difference bound matrices (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 26, 2024 are

• Proofs that the mirror function of binary trees is involutive in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalized programming language with speculative execution. ~ Jamie Wright & Andrei Popescu. #ITP #IsabelleHOL
• Game programming in Prolog (Part 1). ~ Youngjin Kang. #Prolog #LogicProgramming

The readings shared in Mastodon on August 24, 2024 are

• Readings shared August 23, 2024. #ITP #IsabelleHOL #LeanProver #Lean4 #AI #DeepLearning #Haskell #FunctionalProgramming #LogicProgramming #Python
• Logic and computation intertwined. ~ Prabhakar Ragde. #Logic #Racket #ITP #Coq #Agda
• Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. #TypeTheory #CurryHoward

The readings shared in Mastodon on August 23, 2024 are

• Readings shared August 22, 2024. #ITP #Agda #HoTT #Haskell #FunctionalProgramming
• Lean: First steps (06 - Intermediate results). ~ Tariq Rashid. #ITP #Lean4 #Math
• How to make mathematicians into programmers (and vice versa). ~ Will Crichton. #ITP #LeanProver #Math
• Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. ~ Lawrence C Paulson. #ITP #HOL
• Coproduct measure (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang & Xujie Si. #AI #DeepLearning #ITP
• Property-based testing for the people. ~ Harrison Goldstein. #PhDThesis #Haskell #FunctionalProgramming
• Boolean matrix logic programming. ~ Lun Ai & Stephen H. Muggleton. #LogicProgramming
• Ordinals aren't much worse than Quaternions. ~ Philip Zucker. #Python #Math

The readings shared in Mastodon on August 22, 2024 are

• Readings shared August 21, 2024. #ITP #IsabelleHOL #Lean4 #Math #FunctionalProgramming
• Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory. ~ Håkon Robbestad Gylterud, Elisabeth Stenholm & Niccolò Veltri. #ITP #Agda #HoTT
• Prettier. Happier. More Imperative. (Understanding "A prettier printer" by porting it). ~ Benjamin Hodgson. #Haskell #FunctionalProgramming

The readings shared in Mastodon on August 21, 2024 are

• Readings shared August 20, 2024. #ITP #Lean4 #Coq #ACL2 #AlphaProof #Math #Haskell #FunctionalProgramming #Logic #Math #CategoryTheory #TypeTheory
• Probabilistic reasoning and formal proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #Lean4 #FunctionalProgramming
• Worklist algorithms (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL
• Trustworthy verification of realtime systems. ~ Simon Wimmer. #ITP #IsabelleHOL
• Verified model checking of timed automata. ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 20, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus
• Improving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. #ITP #Lean4 #Math #AlphaProof
• Verification and attack synthesis for network protocols. ~ Max von Hippel. #ITP #ACL2
• A two-phase infinite/finite low-level memory model (Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction). ~ Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski & Steve Zdancewic. #ITP #Coq
• Snapshoble stores. ~ Clément Allain, Basile Clément, Alexandre Moine & Gabriel Scherer. #ITP #Coq
• Refinement composition logic. ~ Youngju Song & Dongjae Lee. #ITP #Coq
• Beyond trees: Calculating graph-based compilers (Functional pearl). ~ Patrick Bahr & Graham Hutton. #Haskell #FunctionalProgramming
• An introduction to categorical proof theory. ~ Amirhossein Akbar Tabatabai. #Logic #Math #CategoryTheory #TypeTheory

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #FunctionalProgramming #Math #Prolog #LogicProgramming
• Proofs of the equivalence of reverse definitions in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalisation of the Mathieu-24 group. ~ Edward van de Meent. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 17, 2024. #ITP #LeanProver #Lean4 #Math #AI
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #ITP #LeanProver #Math
• Lean again. ~ Adolfo Neto. #ITP #Lean4 #FunctionalProgramming
• The semantics of metapropramming in Prolog. ~ David S. Warren. #Prolog #LogicProgramming

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 15, 2024. #ITP #IsabelleHOL #Coq #SSReflect #Math #Haskell #Elm #FunctionalProgramming
• Machine-checked proofs and the rise of formal methods in mathematics. ~ Leonardo de Moura. #ITP #LeanProver #Math
• DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. ~ Huajian Xin et als. #ITP #Lean4
• The AI scientist: Towards fully automated open-ended scientific discovery. ~ Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune & David Ha. #AI

The readings shared in Mastodon on August 15, 2024 are

• Readings shared August 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• Software verification with Isabelle/HOL. ~ Peter Höfner. #ITP #IsabelleHOL
• Functional algorithms verified in SSReflect. ~ Alex Gryzlov et als. #ITP #Coq #SSReflect
• Haskell for Elm developers: giving names to stuff (Part 5 - Semigroups and Monoids). ~ Flavio Corpa. #Haskell #Elm #FunctionalProgramming
• The Haskell Unfolder Episode 31: nothunks. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Galois theory. ~ Tom Leinster. #Math

The readings shared in Mastodon on August 14, 2024 are

• Readings shared August 13, 2024. #ITP #Coq #Agda #Math #Python
• #Calculemus: Proofs with Lean4 and Isabelle/HOL of "take n xs ++ drop n xs = xs". #ITP #Lean4 #IsabelleHOL #Math
• Introduction to proofs with Lean proof assistant. ~ Sina Hazratpour. #ITP #LeanProver
• Taller de Lean 4. ~ Enric Cosme, Mario Vago. #ITP #LeanProver #Lean4
• A topological approach for semi-supervised learning. ~ Adrián Inés, César Domínguez, Jónathan Heras, Gadea Mata & Julio Rubio. #AI #MachineLearning #Math

The readings shared in Mastodon on August 13, 2024 are

• Readings Shared August 13, 2024. #Python #Haskell #FunctionalProgramming
• An elementary proof of the FMP for Kleene algebra. ~ Tobias Kappé. #ITP #Coq #Math
• Sharing proofs with predicative theories through universe-polymorphic elaboration. ~ Thiago Felicissimo & Frédéric Blanqui. #ITP #Agda #Coq
• Bounding Euler's constant. ~ Philip Zucker. #Math #Python
• Algebra. It's powerful. But it's not what it was. ~ Keith Devlin. #Math

Las lecturas compartidas en Mastodon el 10 de agosto de 2024 son

• Lecturas compartidas el 9 de agosto de 2024. #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA
• Function composition and currying in Python (Python in the streets, Haskell in the sheets!). ~ Francisco Gutierrez. #Python #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 9 de agosto de 2024 son

• Lecturas compartidas el 8 de agosto de 2024. #ITP #Lean4 #IsabelleHOL #Math #DeepLearning
• A tricky lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Verified transformations for convex programming. ~ Ramon Fernández Mir. #ITP #Lean4 #Math
• First steps towards computational polynomials in Lean. ~ James Harold Davenport. #ITP #LeanProver #Math
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner & Detlef Plump. #ITP #IsabelleHOL
• Validation of a formal floating-point model for the interactive proof assistant Isabelle/HOL. ~ Olof Lindström. #ITP #IsabelleHOL
• Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. #ITP #HOL4
• An in-context learning agent for formal theorem-proving. ~ Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri. #LLMs #ITP #Coq #LeanProver
• Competitive programming in Haskell: Tree path decomposition, part II. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• typedKanren: Statically typed relational programming with exhaustive matching in Haskell. ~ Nikolai Kudasov & Artem Starikov. #Haskell #FunctionalProgramming
• Combinatorial and algorithmic mathematics (From foundation to optimization) ~ Baha M. Alzalg #Math
• Intelligent Computer Mathematics (17th International Conference, CICM 2024, Proceedings) #ITP #Math
• The potential for AI in science and mathematics. ~ Terence Tao. #IA #Math #ITP #LeanProver

Las lecturas compartidas en Mastodon el 08 de agosto de 2024 son

• Lecturas compartidas el 6 de agosto de 2024. #ITP #Coq #Python #FunctionalProgramming
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length(xs ++ ys) = length(xs) + length(ys)". #ITP #Lean4 #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si. #ITP #DeepLearning
• Getting started with Blueprint-Driven formalization projects in Lean. ~ Pietro Monticone. #ITP #LeanProver #Lean4

Las lecturas compartidas en Mastodon el 6 de agosto de 2024 son

• Lecturas compartidas el 5 de agosto de 2024. #ATP #SAT #Haskell #FunctionalProgramming #CurryHoward #TypeScript
• Rely-guarantee semantics for separation-logic-based specification extraction. ~ Paul He. #PhDThesis #ITP #Coq
• Functional programming in Python: When and how to use it. ~ John Sturtz. #Python #FunctionalProgramming

Las lecturas compartidas en Mastodon el 5 de agosto de 2024 son

• Lecturas compartidas el 4 de agosto de 2024. #ITP #IsabelleHOL #Diproche #Math
• A SAT-based approach to rigorous verification of Bayesian networks. ~ Ignacy Stępka, Nicholas Gisolfi & Artur Dubrawski. #ATP #SAT
• Why does everyone hate Haskell, jazz, and pure math? ~ Adam Dueck. #Haskell #FunctionalProgramming
• Proofs are programs: A few examples of the Curry-Howard correspondence. ~ Adam Dueck. #CurryHoward #TypeScript

Las lecturas compartidas en Mastodon el 4 de agosto de 2024 son

• Lecturas compartidas el 3 de agosto de 2024. #Math
• The top-down solver verified: Building confidence in static analyzers. Yannick Stade, Sarah Tilscher & Helmut Seidl. #ITP #IsabelleHOL
• Sociomathematical norms and automated proof checking in mathematical education: Reflections and experiences. ~ Merlin Carl. #ITP #Diproche #Math

Las lecturas compartidas en Mastodon el 3 de agosto de 2024 son

• Lecturas compartidas el 2 de agosto de 2024. #ITP #LeanProver #IsabelleHOL #Coq #MinLog #Agda #Logic #Math #FunctionalProgramming #Haskell #Hope #Miranda
• A guide to writing mathematics. ~ Kevin P. Lee. #Math
• How to write mathematics. ~ Paul R. Halmos. #Math

Las lecturas compartidas en Mastodon el 2 de agosto de 2024 son

• Lecturas compartidas el 1 de agosto de 2024. #ITP #Lean4 #Mathlib #Coq #Math #Haskell #FunctionalProgramming
• Semialgebraic groups and generalized affine buildings. ~ Raphael Appenzeller. #PhDThesis #ITP #LeanProver #Math
• Lie groups and algebras (in Isabelle/HOL). ~ Richard Schmoetten & Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• Semantical analysis of intuitionistic modal logics between CK and IK. ~ Jim de Groot, Ian Shillito & Ranald Clouston. #ITP #Coq #Logic
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis. ~ Grigory Devadze, Victor Magron & Stefan Streif. #ITP #MinLog #Math
• A framework for semiring-annotated type systems. ~ James Wood. #ITP #Agda #TypeTheory
• Where does the name "algebraic data type" come from? ~ Li-yao Xia. #FunctionalProgramming #Hope #Miranda
• Analyzing Haskell stability. ~ Jappie Klooster. #Haskell #FunctionalProgramming
• Data.Maybe, and thoughts on library design. ~ Srijan Paul. #Haskell #FunctionalProgramming
• Esta vez sí: Con la IA, nada será igual en la Universidad. ~ Mariano Fernández Enguita. #IA #Educación
• La demanda de educación superior ante el cambio tecnológico y la inteligencia artificial. ~ José Ignacio Conde-Ruiz, Juan José Ganuza, Manu García y Carlos Victoria. #IA #Educación
• Inteligencia Artificial y capital humano: ¿Pueden estar en peligro sus complementariedades? ~ Juan F. Jimeno y Ana Lamo. #IA

Las lecturas compartidas en Mastodon el 1 de agosto de 2024 son

• Lecturas compartidas el 31 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #LLMs #ATP #Reasoning
• Continuous functions — formalized in Lean4. ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• Continuous functions — formalized in Lean4 (code and a LaTeX document). ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• LeanSearch: Find theorems in Mathlib4 using natural language query. #ITP #Lean4 #Mathlib
• Search Mathlib: A webpage that searches for Mathlib theorems. ~ Deming Xu. #ITP #Lean4 #Mathlib
• Set Theory Game (An introduction to mathematical proof). ~ Daniel J. Velleman./#/g/djvelleman/stg4 #ITP #Lean4 #Math
• Lean Game Server (A repository of learning games for the proof assistant Lean (Lean 4) and its mathematical library Mathlib). #ITP #Lean4 #Math
• A verified foreign function interface between Coq and C. ~ Joomy Korkut, Kathrin Stark, Andrew W. Appel. #ITP #Coq
• The Haskell Unfolder Episode 30: runST. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 31 de julio de 2024 son

• Lecturas compartidas el 30 de julio de 2024. #ITP #IsabelleHOL #Math #LogicProgramming #ASP #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Asociatividad de la concatenación de listas". #ITP #Lean4 #IsabelleHOL #Math
• A formalization and proof checker for Isabelle’s metalogic. ~ Simon Roßkopf, Tobias Nipkow. #ITP #IsabelleHOL
• From Schütte’s formal systems to modern automated deduction. ~ Wolfgang Bibel, Jens Otten. #ATP #Logic
• Steamroller problems: An evaluation of LLM reasoning capability with automated theorem prover strategies. ~ Lachlan McGinness, Peter Baumgartner. #LLMs #ATP #Reasoning

Las lecturas compartidas en Mastodon el 30 de julio de 2024 son

• Lecturas compartidas el 29 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #AI #CAS
• A construction of the Lie algebra of a Lie group in Isabelle/HOL. ~ Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• LLASP: Fine-tuning Large Language Models for Answer Set Programming. ~ Erica Coppolillo, Francesco Calimeri, Giuseppe Manco, Simona Perri, Francesco Ricca. #AI #LLMs #LogicProgramming #ASP
• AlphaProof, AlphaGeometry, ChatGPT, and why the future of AI is neurosymbolic. ~ Gary Marcus. #AI
• CalcGPT, la calculadora inútil pero «inteligente». ~ @Alvy. #ChatGPT #Math

Las lecturas compartidas en Mastodon el 29 de julio de 2024 son

• Lecturas compartidas el 28 de julio de 2024. #ITP #LeanProver #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length (replicate n x) = n". #ITP #Lean4 #IsabelleHOL #Math
• Advancing mathematics through computers and AI: Automation, discovery, and collaboration. ~Douglas C. Youvan. #AI #ITP #CAS #Math

Las lecturas compartidas en Mastodon el 28 de julio de 2024 son

• Lecturas compartidas el 27 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Formalisation of the finite simple Conway groups in Lean. ~ Erik van der Plas. #ITP #LeanProver #Math
• The first Janko group J1: simplicity and formalization. ~ Roxy van de Kuilen. #ITP #LeanProver #Math

Las lecturas compartidas en Mastodon el 27 de julio de 2024 son

• Lecturas compartidas el 26 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #IMO #AI #AlphaProof #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n". #ITP #Lean4 #IsabelleHOL #Math
• Haskell nuggets: k-means. ~ Justin Lê. #FunctionalProgramming #Haskell
• Prove or disprove. 100 conjectures from the OEIS. ~ Ralf Stephan. #Math

Las lecturas compartidas en Mastodon el 26 de julio de 2024 son

• Lecturas compartidas el 25 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones divergentes positivas no tienen límites finitos". #ITP #Lean4 #IsabelleHOL #Math
• AI achieves silver-medal standard solving International Mathematical Olympiad problems. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Google DeepMind IMO 2024 Solutions. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Move over, mathematicians, here comes AlphaProof (A.I. is getting good at math — and might soon make a worthy collaborator for humans). ~ Siobhan Roberts. #AI #Math #IMO #Lean4 #AlphaProof
• To formalized mathematics and back with the Lean theorem prover. ~ Kyle Miller. #ITP #LeanProver #Math
• The mysteries and frustrations of numerical proofs. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Formal verification of 2-3 trees in Coq. ~ Horia-Matei Cornea. #ITP #Coq
• Rivers: eventually constant streams in Haskell. ~ Brent Yorgey. #FunctionalProgramming #Haskell
• Types as interfaces. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 25 de julio de 2024 son

• Lecturas compartidas el 24 de julio de 2024. #ITP #Lean4 #Coq #Logic #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u". #ITP #Lean4 #IsabelleHOL #Math
• Approximate relational reasoning for higher-order probabilistic programs. ~ Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal. #ITP #Coq
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover. ~ Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen. #LLMs #ITP #Lean4 #Math

Las lecturas compartidas en Mastodon el 24 de julio de 2024 son

• Lecturas compartidas el 23 de julio de 2024. #ITP #Lean4 #Math #FunctionalProgramming #OCaml
• Lean For Haskell developers. ~ Solomon. #ITP #Lean4 #FunctionalProgramming #Haskell
• A logic for veracity: Development and implementation. ~ Daniel Britten, Steve Reeves. #ITP #Coq #Logic
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue, Takafumi Saikawa. #ITP #Coq

Las lecturas compartidas en Mastodon el 23 de julio de 2024 son

• Lecturas compartidas el 22 de julio de 2024. #AI
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean. ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean (Code). ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• (Pro)Seminar on computer-assisted mathematics. ~ Judith Ludwig, Florent Schaffhauser. #CAS #Sage #ITP #LeanProver #Math
• Practical deductive verification of OCaml programs (Extended version). ~ Mário Pereira. #FunctionalProgramming #OCaml

Las lecturas compartidas en Mastodon el 22 de julio de 2024 son

• Lecturas compartidas el 21 de julio de 2024. #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell
• Un robot que resuelve rompecabezas 200 veces más rápido que las personas más hábiles. ~ @Alvy. #AI

Las lecturas compartidas en Mastodon el 21 de julio de 2024 son

• Lecturas compartidas el 20 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Logic #CompSci
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• A tree rewriting system for the Reflection Calculus. ~ Sofía Santiago-Fernández, Joost J. Joosten, David Fernández-Duque. #ITP #Coq #Logic
• Automated proof tactics for model transformation. ~ Julien Cohen, Massimo Tisi, Remi Douence. #ITP #Coq
• Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. #FunctionalProgramming #Haskell #LiquidHaskell
• Monumental proof settles geometric Langlands conjecture. ~ Erica Klarreich. #Math

Las lecturas compartidas en Mastodon el 20 de julio de 2024 son

• Lecturas compartidas el 19 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin, Zhiqing Sun, Yiming Yang, Sean Welleck. #ITP #Lean4 #LLMs
• PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition. ~ George Tsoukalas et als. #LLMs #ITP #Lean4 #IsabelleHOL #Coq
• Haskelite: A tracing interpreter based on a pattern-matching calculus. ~ Pedro Vasconcelos, Rodrigo Marques. #FunctionalProgramming #Haskell
• Higher-order specifications for deductive synthesis of programs with pointers. ~ David Young et als. #FunctionalProgramming #Pika
• The significance of symbolic logic for scientific education. ~ André Platzer. #Logic #CompSci

Las lecturas compartidas en Mastodon el 19 de julio de 2024 son

• Lecturas compartidas el 18 de julio de 2024. #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "El punto de acumulación de las sucesiones convergente es su límite". #ITP #Lean4 #IsabelleHOL #Math
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als. #ITP #Lean4 #Math
• Haskell for dilettantes, Part 1: Intro. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 2: Expressions, types, and functions. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 3a: Homework 1, Exercise 1. ~ Tea Leaves. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 18 de julio de 2024 son

• Lecturas compartidas el 16 de julio de 2024. #ITP #Lean4 #Coq #LLMs #Programming #Emacs
• Functional Pearl: Short and mechanized logical relation for dependent type theories. ~ Yiyun Liu, Stephanie Weirich. #ITP #Coq
• HHLPar: Automated theorem prover for parallel hybrid communicating sequential processes. ~ Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan. #ITP #IsabelleHOL
• Molly: A verified compiler for cryptographic roles. ~ Daniel J. Dougherty, Joshua D. Guttman. #ITP #Coq
• Formalizing operads for a categorical framework of DSL composition. ~ Zachary Flores, Angelo Taranto, Yakir Forman, Eric Bond. #ITP #Coq
• Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. #FunctionalProgramming #LiquidHaskell
• Demystifying Artificial Intelligence (Symbolic, data-driven, statistical and ethical AI). ~ Emmanuel Gillain (ed.). #eBook #AI
• Using ChatGPT as a proof assistant in a mathematics pathways course. ~ Hyejin Park, Eric D. Manley. #ChatGPT #Math #Reasoning
• The Haskell Unfolder Episode 29: Exceptions, annotations and backtraces. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 16 de julio de 2024 son

• Lecturas compartidas el 15 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #CompSci #Haskell #Prolog
• A term-patching framework for eliminating definitional equalities in Lean (Work-in-progress). ~ Rishikesh Vaishnav. #ITP #Lean4
• Guided proof search using large language models and lemma extraction in Coq. ~ Tarun Prasad. #ITP #Coq #LLMs
• Code completion with Google Gemini for Emacsen. ~ Hitoshi Uchida. #Programming #Emacs #Gemini

Las lecturas compartidas en Mastodon el 15 de julio de 2024 son

• Lecturas compartidas el 14 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Haskell #Prolog
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las subsucesiones tienen el mismo límite que la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• Formalizing implicational axiomatics for classical first-order logic with functions in Isabelle/HOL. ~ Jørgen Villadsen, Roberto Pettinau. #ITP #IsabelleHOL #Logic
• Mathematics in programming. ~ Xinyu Liu #Math #CompSci #Haskell
• Smart investment problem with Prolog. ~ Matteo Redaelli. #Prolog

Las lecturas compartidas en Mastodon el 14 de julio de 2024 son

• Lecturas compartidas el 13 de julio de 2024. #ITP #Lean4 #Coq #Abella #Agda #Mizar #Logic #Math #IMO #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]". #ITP #Lean4 #IsabelleHOL #Math
• Implementing the Fatio protocol for multi-agent argumentation in LogiKEy. ~ Luca Pasetto, Christoph Benzmüller. #Logic #ITP #IsabelleHOL
• Implementing intermediate logics. ~ Bastiaan Haaksema, Jens Otten, Revantha Ramanayake. #ATP #Logic #Haskell #Prolog

Las lecturas compartidas en Mastodon el 14 de julio de 2024 son

• Lecturas compartidas el 12 de julio de 2024. #ITP #Coq #Logic #Math #FunctionalProgramming #Haskell #Physics
• IMO 1987 Problem 4: Animated Lean 4 proof. ~ David Renshaw. #ITP #Lean4 #Math #IMO
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu. #ITP #Coq #Logic #Math
• Binding contexts as partitionable multisets in Abella. ~ Terrance Gray, Gopalan Nadathur. #ITP #Abella
• Domain theory in univalent foundations I: Directed complete posets and Scott's D∞. ~ Tom de Jong. #ITP #Agda
• Domain theory in univalent foundations II: Continuous and algebraic domains. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda
• Separable polynomials and separable extensions. ~ Christoph Schwarzweller. #ITP #Mizar #Math
• Integral of continuous three variable functions. ~ Noboru Endou. #ITP #Mizar #Math
• Competitive programming in Haskell: Tree path decomposition, part I. ~ Brent Yorgey. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 12 de julio de 2024 son

• Lecturas compartidas el 11 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• Functional programming in learning electromagnetic theory. ~ Scott N. Walck. #FunctionalProgramming #Haskell #Physics
• Building a data compression utility in Haskell using Huffman codes. ~ Marcelo Lazaroni. #FunctionalProgramming #Haskell
• Collatz computations in base 2 and 3. ~ Chris Smith. #FunctionalProgramming #Haskell #Math
• The flower calculus. ~ Pablo Donato. #ITP #Coq #Logic

Las lecturas compartidas en Mastodon el 11 de julio de 2024 son

• Lecturas compartidas el 10 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Abella #Beluga #Agda #Haskell #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las funciones de extracción no están acotadas". #ITP #Lean4 #IsabelleHOL #Math

Las lecturas compartidas en Mastodon el 10 de julio de 2024 son

• Lecturas compartidas el 9 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Relación entre los índices de las subsucesiones y de la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• On non-triviality of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu. #ITP #Coq
• Binding contexts as partitionable multisets in Abella. ~ Terrance Gray, Gopalan Nadathur. #ITP #Abella
• A Beluga formalization of the Harmony Lemma in the π-calculus. ~ Gabriele Cecilia, Alberto Momigliano. #ITP #Beluga
• Confluence by the Z-property for De Bruijn’s λ-calculus with nameless dummies, based on PLFA∗. ~ Vincent van Oostrom. #ITP #Agda
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, Tobias Grosser. #ITP #Lean4
• Moca 0.3: A first-order theorem prover for Horn clauses. ~ Yusuke Oi, Nao Hirokawa, Teppei Saito. #Haskell #ATP #Logic

Las lecturas compartidas en Mastodon el 9 de julio de 2024 son

• Lecturas compartidas el 8 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones de equivalencia". #ITP #Lean4 #IsabelleHOL #Math
• Lean: First steps (05 - Inequalities). ~ Tariq Rashid. #ITP #Lean4 #Math
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #Lean4
• Normative conditional reasoning as a fragment of HOL. ~ Xavier Parent, Christoph Benzmüller. #ITP #IsabelleHOL #Logic

Las lecturas compartidas en Mastodon el 8 de julio de 2024 son

• Lecturas compartidas el 7 de julio de 2024. #ITP #IsabelleHOL #Lean4 #Coq #Agda #Math #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones transitivas". #ITP #Lean4 #IsabelleHOL #Math
• Mechanised uniform interpolation for modal logics K, GL, and iSL. ~ Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito. #ITP #Coq #Logic

Las lecturas compartidas en Mastodon el 7 de julio de 2024 son

• Lecturas compartidas el 6 de julio de 2024. #ITP #Coq #Math
• Lean: Past, present, and future. ~ Sebastian Ullrich. #ITP #Lean4
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als. #ITP #Lean4 #Math
• A Lean formalization of Cedar. ~ Bhakti Shah. #ITP #Lean4
• A verified algorithm for deciding pattern completeness. ~ René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL #Haskell
• On synthesising Linux kernel module components from Coq formalisations. ~ Mario Frank. #PhDThesis #ITP #Coq
• Monads, comonads, and transducers. ~ Rafał Stefański. #ITP #Coq
• Machine-checked categorical diagrammatic reasoning. ~ Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez. #ITP #Coq
• Mechanized subject expansion in uniform intersection types for perpetual reductions. ~ Andrej Dudenhefner, Daniele Pautasso. #ITP #Coq
• Substitution for non-wellfounded syntax with binders through monoidal categories. ~ Ralph Matthes, Kobe Wullaert, Benedikt Ahrens. #ITP #Coq
• Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Émile Oleon. #ITP #Agda #Math

Las lecturas compartidas en Mastodon el 6 de julio de 2024 son

• Lecturas compartidas el 5 de julio de 2024. #ATP #ITP #IsabelleHOL #Lean4 #Logic #Math #FunctionalProgramming #Haskell #OCaml
• With fifth busy beaver, researchers approach computation’s limits (After decades of uncertainty, a motley team of programmers has proved precisely how complicated simple computer programs can get). ~ Ben Brubaker. #ITP #Coq #Math

Las lecturas compartidas en Mastodon el 5 de julio de 2024 son

• Lecturas compartidas el 4 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las familias de conjuntos definen relaciones simétricas". #ITP #Lean4 #IsabelleHOL #Math
• Automated reasoning for mathematics. ~ Jeremy Avigad. #ATP #ITP #Math
• Fast and verified UNSAT certificate checking. ~ Peter Lammich. #ITP #IsabelleHOL #SAT
• Formalizing chemical physics using the Lean theorem prover. ~ Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, Tyler R. Josephson. #ITP #Lean4
• Formalising Fermat’s last theorem for exponent 3 in Lean. ~ Pietro Monticone. #ITP #Lean4 #Math
• Verificació formal de formes equivalents de l’axioma d’elecció. ~ Vicent Pons Llopis. #TFG #ITP #Lean4 #Math
• An empirical assessment of progress in automated theorem proving. ~ Geoff Sutcliffe et als. #ATP
• Lemma discovery and strategies for automated induction. ~ Sólrún Halla Einarsdóttir, Márton Hajdu, Moa Johansson, Nicholas Smallbone, Martin Suda. #FunctionalProgramming #Haskell
• A technological approach to teaching inequalities, propositional and predicate logic. ~ Zoltán Kovács, Reinhard Oldenburg. #Logic #GeoGebra
• A natural-language proof assistant for higher-order logic (Work in progress). ~ Adam Dingle. #ITP #Natty #OCaml
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #OCaml
• Learning formal mathematics from intrinsic motivation. ~ Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman. #Math #AI
• The sad state of property-based testing libraries. ~ #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 4 de julio de 2024 son

• Lecturas compartidas el 3 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las particiones definen relaciones reflexivas". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Número de divisores. #Haskell #Python #Matemáticas
• Lean: First steps. #ITP #Lean4 #Math
• TheoremLlama: Transforming general-purpose LLMs into Lean4 experts. ~ Ruida Wang et als. #ITP #Lean4 #LLMs
• The Haskell Unfolder Episode 28: Type families and overlapping instances. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 3 de julio de 2024 son

• Lecturas compartidas el 2 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #CategoryTheory #FunctionalProgramming #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las clases de equivalencia de elementos no relacionados son disjuntas". #ITP #Lean4 #IsabelleHOL #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "El conjunto de las clases de equivalencia es una partición". #ITP #Lean4 #IsabelleHOL #Math

Las lecturas compartidas en Mastodon el 2 de julio de 2024 son

• Lecturas compartidas el 1 de julio de 2024. #ITP #IsabelleHOL #Lean4 #Math #AI #MachineLearning #DeepLearning
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las clases de equivalencia de elementos relacionados son iguales". #ITP #Lean4 #IsabelleHOL #Math
• Extending Isabelle/HOL's code generator with support for the Go programming language. ~ Terru Stübinger, Lars Hupel. #ITP #IsabelleHOL
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt, Zachary Stone. #ITP #Coq #Math
• This month in Mathlib (May 2024). #ITP #Lean4 #Mathlib #Math
• Folding in parallel. ~ Oleg Kiselyov. #FunctionalProgramming #Haskell
• Python's built-in functions: A complete exploration. ~ Leodanis Pozo Ramos. #Python #Programming
• Introducing category theory. ~ Peter Smith. #CategoryTheory

Las lecturas compartidas en Mastodon el 1 de julio de 2024 son

• Lecturas compartidas el 30 de junio de 2024. #ITP #IsabelleHOL #Math #Haskell #Python
• Formalized synthetic geometry. ~ André Hernández-Espiet. #PhDThesis #ITP #Lean4 #Math
• Verification using formalised mathematics and theorem proving of reinforcement and deep learning. ~ Mark Chevallier. #ITP #IsabelleHOL #DeepLearning
• AI for Mathematics (AI4Math) paper list. ~ Haocheng Ju. #AI #Math #ITP #MachineLearning

Las lecturas compartidas en Mastodon el 30 de junio de 2024 son

• Lecturas compartidas el 29 de junio de 2024. #ITP #Lean4 #IsabelleHOL #PVS #Coq #Logic #Math #Haskell #Python
• #Exercitium: Conjunto de divisores. #Haskell #Python #Matemáticas
• The accompanying code for the submission "Formalising half of a graduate textbook on number theory" to ITP 2024. ~ Manuel Eberl, Anthony Bordg, Lawrence Paulson, and Wenda Li. #ITP #IsabelleHOL #Math
• Nine chapters of analytic number theory in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math