The readings shared in Mastodon on September 27, 2024 are

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

The readings shared in Mastodon on September 25, 2024 are

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

The readings shared in Mastodon on September 24, 2024 are

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

The readings shared in Mastodon on September 23, 2024 are

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

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 (@rzeta0@mastodon.social). #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 (@marcmasdeu) et als. #ITP #LeanProver #Lean3 #Math
• Formalization of Riemann-Stieltjes integral in Lean4. ~ Marc Masdeu (@marcmasdeu) 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 (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #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