The readings shared in Bluesky on 15 February 2025 are

• Prospects for formalizing the theory of weak infinite-dimensional categories. ~ Emily Riehl. #ITP #LeanProver #Math

The readings shared in Bluesky on 14 February 2025 are

• Language models for verifiable mathematical automation (Interaction, integration, and autoformalization). ~ Qiaochu Jiang. #ITP #IsabelleHOL #LLMs #Autoformalization
• The Haskell Unfolder Episode 39: Deriving strategies). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 13 February 2025 are

• A Coq formalization of unification modulo exclusive-or. ~ Yichi Xu, Daniel J. Dougherty, Rose Bohrer. #ITP #Coq
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• A proof of Hilbert basis theorem and an extension to formal power series (in Isabelle/HOL). ~ Benjamin Puyobro, Benoît Ballenghien, Burkhart Wolff. #ITP #IsabelleHOL #Math
• Why Amazon is betting on 'automated reasoning' to reduce AI's hallucinations. ~ Belle Lin. #AI #LLMs #ITP
• On LLM-generated logic programs and their inference execution methods. ~ Paul Tarau. #LLMs #LogicProgramming #Prolog
• LP-LM: No hallucinations in question answering with logic programming. ~ Katherine Wu, Yanhong A. Liu. #LLMs #LogicProgramming #Prolog
• Improving autoformalization using type checking. ~ Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut. #Autoformalization #LLMs #ITP #LeanProver #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper et als. #LLMs #Math
• A model for learning-curve estimation in efficient neural architecture search and its application in predictive health maintenance. ~ David Solís-Martín, Juan Galán-Páez, Joaquín Borrego-Díaz. #AI
• 50 years of programming language evolution through the software Heritage looking glass. ~ Adèle Desmazières, Roberto Di Cosmo, Valentin Lorentz. #Programming

The readings shared in Bluesky on 12 February 2025 are

• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #LLMs #ITP #LeanProver #IsabelleHOL
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming

The readings shared in Bluesky on 11 February 2025 are

• Examining false positives under inference scaling for mathematical reasoning. ~ Yu Wang, Nan Yang, Liang Wang, Furu Wei. #LLMs #Math #Reasoning
• MATH-perturb: Benchmarking LLMs' math reasoning abilities against hard perturbations. ~ Kaixuan Huang et als. #LLMs #Math #Reasoning
• Embedding self-correction as an inherent ability in large language models for enhanced mathematical reasoning. ~ Kuofeng Gao, Huanqia Cai, Qingyao Shuai, Dihong Gong, Zhifeng Li. #LLMs #Math #Reasoning
• Streams in Common Lisp. ~ jcs. #CommonLisp
• Functional streams. ~ Atabey Kaygun. #CommonLisp
• Programming techniques: Generating prime numbers in Common Lisp. ~ Mitchell Chung. #CommonLisp #Math

The readings shared in Bluesky on 10 February 2025 are

• Feedback loops guide AI to proof checking. ~ Chris Edwards. #AI #ITP #LeanProver #Coq
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li, Conor Duggan, Curtis Bright, Vijay Ganesh. #SAT #CAS
• Proving the coding interview: A benchmark for formally verified code generation. ~ Quinn Dougherty, Ronak Mehta. #AI #LLMs #Python #ITP
• ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data. ~ Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo. #LLMs #ITP #LeanProver #Math #Autoformalization
• Can Transformers reason logically? A study in SAT solving. ~ Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee. #LLMs #Reasoning #SAT_Solvers
• #Exercitium: Anagramas. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 9 February 2025 are

• What is a quotient? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Systems correctness practices at AWS: Leveraging formal and semi-formal methods. ~ Marc Brooker, Ankush Desai. #FormalMethods #ITP #LeanProver
• Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Chatbot software begins to face fundamental limitations. ~ Anil Ananthaswamy. #LLMs

The readings shared in Bluesky on 8 February 2025 are

• Verification of the CVM algorithm with a new recursive analysis technique. ~ Emin Karayel, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan, Seng Joe Watt. #ITP #IsabelleHOL
• Review of "Haskell in depth" by Vitaly Bragilevsky. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Cervantes, la cuadratura del círculo y la búsqueda del punto fijo. ~ Tomás Domínguez Benavides. #Matemáticas

The readings shared in Bluesky on 6 February 2025 are

• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han, Taeil Hur, Youngmi Hur, Kathy Sangkyung Lee, Myungyoon Lee, Hyojae Lim. #LLMs #ChatGPT #ITP #LeanProver
• Elisp cheatsheet for Python programmers. ~ Charles Choi. #Python #Emacs #Elisp
• La categoría de conjuntos abstractos. ~ Luis Turcio. #CategoryTheory
• Exercitium: Diagonales principales. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 5 February 2025 are

• On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. #ITP #LeanProver #Mathlib
• Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. #LLMs #ITP #LeanProver
• New proofs probe the limits of mathematical truth. ~ Joseph Howlett. #Math

The readings shared in Bluesky on 4 February 2025 are

• Readings shared February 3, 2025. #ITP #LeanProver #IsabelleHOL #Haskell #Python #CommonLisp #Maxima #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 3 February 2025 are

• A comprehensive survey of the Lean 4 theorem prover: Architecture, applications, and advances. ~ Xichen Tang. #ITP #LeanProver
• Differential privacy (in Isabelle/HOL). ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• Differential privacy using quasi-Borel spaces. ~ Michikazu Hirata. #ITP #IsabelleHOL
• Maxima in the browser using Embedded Common Lisp on WASM. #Maxima #CoomonLisp #Math
• #Exercitium: La bandera tricolor. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 2 February 2025 are

• Transitive union-closed families (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller, Dana Scott. #ITP #IsabelleHOL
• DeepSeek: A breakthrough in AI for math (and everything else). ~ David H Bailey. #DeepSeek #Math
• Some lessons from the OpenAI-FrontierMath debacle. ~ 7vik. #AI #Math
• Kazimierz Kuratowski, el talento y el compromiso de un matemático de Varsovia. ~ Marta Macho Stadler. #Math

The readings shared in Bluesky on 1 February 2025 are

• The continuous functional calculus in Lean. ~ Anatole Dedecker, Jireh Loreaux. #ITP #LeanProver #Math
• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• Formally verified binary-level pointer analysis. ~ Freek Verbeek, Ali Shokri, Daniel Engel, Binoy Ravindran. #ITP #IsabelleHOL
• A formal semantics of Core Erlang. ~ Ibrahim Abdelrahman Mohamedi. #ITP #IsabelleHOL #Erlang
• Context-dependent effects in guarded interaction trees. ~ Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal. #ITP #Coq
• Reasoning about weak isolation levels in separation logic. ~ Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal. #ITP #Coq
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu. #AI #LLMs #ITP #LeanProver #Math
• How to recognize artificial mathematical intelligence in theorem proving. ~ Markus Pantsar. #AI #Math #ITP
• LemmaHead: RAG assisted proof generation using large language models. ~ Tianbo Yang, Mingqi Yang, Hongyi Zhao, Tianshuo Yang. #AI #LLMs #ITP #LeanProver #Math
• Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. #LLMs #Reasoning #SMT #Z3
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #AI #LLMs #ITP #Coq #LeanProver #Math

The readings shared in Bluesky on 31 January 2025 are

• Solidifying modern SMT solvers. ~ Dominik Winterer. #SMT
• The Common Lisp Cheat Sheet. ~ Ashok Khanna. #CommonLisp
• #Exercitium: Ordenación por el máximo. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 30 January 2025 are

• Readings shared January 29, 2025. #ITP #IsabelleHOL
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Analytic number theory exponent database. ~ Terence Tao et als. #ITP #LeanProver #Math
• Cellular methods in homotopy type theory. ~ Axel Ljungström, Loïc Pujet. #ITP #Agda

The readings shared in Bluesky on 29 January 2025 are

• Readings shared January 28, 2025. #ITP #LeanProver #Logic #Math #Prolog #LogicProgramming #Racket #FunctionalProgramming
• Mission-time linear temporal logic (in Isabelle/HOL). ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan. #ITP #IsabelleHOL
• Mission-time linear temporal logic to regular expressions (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian. #ITP #IsabelleHOL

The readings shared in Bluesky on 28 January 2025 are

• Readings shared January 26, 2025. #ITP #LeanProver #HOL_Light #Math
• The directed Van Kampen Theorem in Lean. ~ Henning Basoldm, Peter Bruin, Dominique Lawson. #ITP #LeanProver #Math
• The simplicity of Prolog. ~ Ties Westendorp. #Prolog #LogicProgramming
• Beautiful Racket (An introduction to language-oriented programming using Racket). ~ Matthew Butterick. #Racket #FunctionalProgramming
• New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili./#/g/jadabouhawili/knightsandknaves-lean4game #ITP #LeanProver
• Lean for scientists and engineers. ~ Tyler Josephson. #ITP #LeanProver
• lean-mine: A collection of problems solved in Lean. #ITP #LeanProver #Math
• Baby Rudin project: An attempt to formalize every problem in Baby Rudin with natural language description. #ITP #LeanProver #Math
• Homo ratiocinator (Reckoning human). ~ Moshe Vardi. #Logic #Math

The readings shared in Bluesky on 26 January 2025 are

• Readings shared January 25, 2025. #ITP #Agda #Coq #Rocq #IsabelleHOL #Math #FunctionalProgramming #Haskell #JuliaLang
• Certified knowledge compilation with application to formally verified model counting. ~ Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule. #ITP #LeanProver
• Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. #ITP #HOL_Light #Math
• Math Encounters: "You want proof? I'll give you proof! (Mathematical arguments from Euclid to Lean)". ~ Jeremy Avigad. #ITP #LeanProver #Math

The readings shared in Bluesky on 25 January 2025 are

• Readings shared January 24, 2025. #ITP #IsabelleHOL #Haskell #FunctionalProgramming #AI #LLMs #GenerativeAI #NeuroSymbolicAI
• Pinpointing the learning obstacles of an interactive theorem prover. ~ Sára Juhošová, Andy Zaidman, Jesper Cockx. #ITP #Agda
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Combinatorial q-analogues (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Theta functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• The Rogers–Ramanujan identities (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Use monoids for construction. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Calculus for the modern engineer: Putting the joy back in learning advanced mathematics. ~ Jessy Grizzle. #Math #JuliaLang
• Calculus for the modern engineer (Textbook). ~ Jessy Grizzle et als. #Math #JuliaLang #LLMs

The readings shared in Bluesky on 24 January 2025 are

• Readings shared January 23, 2025. #ITP #IsabelleHOL #LeanProver #Python #Programming #Math #AI #LLMs
• Formally verified neurosymbolic trajectory learning via tensor-based linear temporal logic on finite traces. ~ Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #NeuroSymbolicAI
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Fast Haskell, Redux. ~ Jared Tobin. #Haskell #FunctionalProgramming
• Making my life easier with GADTs. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Making my life harder with GADTs. Matt Parsons. #Haskell #FunctionalProgramming
• Making my life easier with two GADTs. ~ borar. #Haskell #FunctionalProgramming
• Modeling dataframes in Haskell using higher-kinded types. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• Supercede’s house style for Haskell. ~ Jezen Thomas. #Haskell #FunctionalProgramming
• Tracing foreign function invocations. ~ Edsko de Vries, Zubin Duggal, Matthew Pickering. #Haskell #FunctionalProgramming
• What I've learned about writing AI apps so far. ~ Laurie Voss. #AI #LLMs
• AI mistakes are very different than human mistakes. ~ Bruce Schneier, Nathan E. Sanders. #AI #LLMs #GenerativeAI
• Cómo trabajar en el día a día con una IA y no morir en el intento. ~ @Alvy. #AI #LLMs
• DeepSeek: un nuevo modelo de IA especializado en razonamiento lógico, resolución de problemas y con licencia abierta MIT. No tiene nada que envidiar a los de OpenAI. ~ @Alvy. #AI #LLMs #DeepSeek
• DeepSeek: Into the unknown (Free access to DeepSeek-V3). #AI #LLMs #DeepSeek

The readings shared in Bluesky on 23 January 2025 are

• Readings shared January 22, 2025. #ITP #IsabelleHOL #Coq #Rocq #LeanProver #FunctionalProgramming #Haskell #Python #Math #AI
• Formalising an easy proof: Dirichlet's approximation theorem. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Hallucination detection and recovery: Initial experiment. ~ GasStationManager. #LLMs #ITP #LeanProver
• Advanced Python course. ~ Michael Foord. #Python #Programming
• ELIZA, la primera psicoterapeuta programada con IA, rescatada del olvido gracias a la arqueología informática. ~ @Alvy. #IA

The readings shared in Bluesky on 22 January 2025 are

• Readings shared January 21, 2025. #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
• #Exercitium: Iguales al siguiente. #Haskell #Python #Matemáticas
• Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Advent of Code 2024: Haskell solution reflections for all 25 days. ~ Justin Le. #Haskell #FunctionalProgramming
• Scientific computing in Lean. ~ Tomas Skrivan. #ITP #LeanProver #Math
• Alpha-beta pruning explored, extended and verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• Can a computer judge interestingness? ~ Michael Douglas. #AI #Math
• Formalising real algebraic geometry. ~ Artie Khovanov, Michael Nedzelsky, Wenda Li. #ITP #IsabelleHOL #Math
• The Mandelbrot set is connected (and other Lean explorations). ~ Geoffrey Irving. #ITP #LeanProver #Math
• Formalising theory of combinatorial optimisation. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
• Condensed type theory. ~ Johan Commelin. #ITP #LeanProver #Math
• How to prove Fermat's Last Theorem. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Structures in dependent type theory. ~ Jeremy Avigad. #ITP #LeanProver
• Comparative formalisation of Kneser's theorem. ~ Mantas Bakšys, Yaël Dillies. #ITP #IsabelleHOL #LeanProver #Math
• Lawvere theories in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
• How to teach Fourier analysis to a large library of formalised mathematics. ~ Yaël Dillies. #ITP #LeanProver #Math
• Computer algebra and the formalisation of new mathematics. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• New Foundations: the story of a large formalisation project. ~ Sky Wilshaw. #ITP #LeanProver #Math
• The mathematics of Artificial Intelligence. ~ Gabriel Peyré. #AI #Math
• The Ramanujan Library (Automated discovery on the hypergraph of integer relations). ~ Itay Beit-Halachmi, Ido Kaminer. #Math #CompSci
• Wikenigma: An encyclopedia of unknowns. #Math #CompSci

The readings shared in Bluesky on 21 January 2025 are

• Readings shared January 20, 2025. #ITP #LeanProver #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #CommonLisp #JanetLang #AI #LLMs #Programming
• Proofs of the Praeclarum Theorema in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing domino tilings with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Think of a number. ~ Kevin Buzzard. #AI #LLMs #Math
• Negatively associated random variables (in Isabelle/HOL). ~ Emin Karayel. #ITP #IsabelleHOL #Math
• Las series de Kempner, o qué ocurre cuando quito un dígito. ~ Miguel Ángel Morales. #Matemáticas

The readings shared in Bluesky on 20 January 2025 are

• Readings shared January 19, 2025. #ITP #LeanProver #FunctionalProgramming #Haskell #AI #LLMs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #Python #Matemáticas
• Classifying the groups of order pq in Lean. ~ Scott Harper, Peiran Wu. #ITP #LeanProver #Math
• Certifying rings of integers in number fields. ~ Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen. #ITP #LeanProver #Math
• Lean: First steps (22 - Recursion). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• [Lean: First steps (22 - Recursion) Video]. ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Lean Together 2025. #ITP #LeanProver
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abzulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Interpreting Brainfuck in Haskell. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Hasochism: The pleasure and pain of dependently typed Haskell programming. ~ Sam Lindley, Conor McBride. #Haskell #FunctionalProgramming
• An efficient algorithm for permutation iteration using a singly linked list. ~ Thomas Baruchel. #CommonLisp #Algorithms
• Janet: a functional and imperative programming language. #JanetLang #FunctionalProgramming
• Janet for mortals (a real book). ~ Ian Henry. #JanetLang #FunctionalProgramming
• Bauble: A playground for making 3D art with lisp and math. ~ Ian Henry et als. #JanetLang #FunctionalProgramming
• Building Bauble. ~ Ian Henry #JanetLang #FunctionalProgramming
• Awesome Janet: Curated list of libraries and tooling for the Janet programming language. ~ Matthew Carter. #JanetLang #FunctionalProgramming
• How developers interact with AI: A taxonomy of human-AI collaboration in software engineering. ~ Christoph Treude, Marco A. Gerosa. #AI #LLMs #Programming

The readings shared in Bluesky on 19 January 2025 are

• Readings shared January 18, 2025. #Haskell #Python #CommonLisp #ITP #Coq #Rocq #Logic #Math #AI #MachineLearning #LLMs
• A toy example of a verified compiler. ~ Marcus Rossel. #ITP #LeanProver
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgrammingo
• Foundations of Large Language Models. ~ Tong Xiao, Jingbo Zhu. #eBook #AI #LLMs
• Language models and structured data. ~ Mehwish Alam. #LLMs

The readings shared in Bluesky on 18 January 2025 are

• Readings shared January 17, 2025. #Haskell #Python #ITP #Coq #Rocq #LeanProver #Logic #Math #AI #LLMs #Reasoning
• #Exercitium: Mastermind. #Haskell #Python #Matemáticas
• Formal proofs in applied mathematics: A Coq formalization of simplicial Lagrange finite elements. ~ Houda Mouhcine. #ITP #Coq #Rocq #Math
• Neurosymbolic tools for effective coding and debugging. ~ Georgios Sakkas. #AI #MachineLearning #LLMs
• Iteration. ~ Joe Marshall. #CommonLisp
• Lisp tutorial. ~ Daniel Nussenbaum. #CommonLisp
• Release Common Lisp on your first day. ~ Dan's Musings. #CommonLisp
• Listopia: List manipulation library inspired by Haskell package Data.List. ~ Ito Dimercel. #CommonLisp #Haskell
• Lisp programming language (Full course for beginners). ~ Alberto Lerda. #CommonLisp
• Neuro symbolic reasoning and learning. ~ Paulo Shakarian, Chitta Baral, Gerardo I. Simari, Bowen Xi, Lahari Pokala. #Logic #AI #MachineLearning
• How I program with LLMs. ~ David Crawshaw. #LLMs #Programming

The readings shared in Bluesky on 17 January 2025 are

• Readings shared January 16, 2025. #ITP #LeanProver #Agda #Logic #Math #SAT #SMT #FunctionalProgramming #Haskell #Python #Matemáticas #AI #LLMs
• #Exercitium: Determinación de los elementos minimales. #Haskell #Python #Matemáticas
• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq #Logic
• Scaling mathlib: tooling and automation for an ever-growing mathematics library. ~ Michael Rothgang. #ITP #LeanProver
• Progress report on the Carleson Project. ~ Floris van Doorn. #ITP #LeanProver #Math
• Egg: An equality saturation tactic in Lean. ~ Marcus Rossel et als. #ITP #LeanProver
• lean-SMT. ~ Abdalrhman Mohamed. #ITP #LeanProver
• Toward functor quasi-categories in Lean. ~ Jack McKoen. #ITP #LeanProver
• Verified foundations for differential privacy. ~ Jean-Baptiste Tristan. #ITP #LeanProver
• Can AI models reason: Is data all you need? ~ Wayne Joubert. #AI #LLMs #Reasoning

The readings shared in Bluesky on 16 January 2025 are

• Readings shared January 15, 2025. #ITP #LeanProver #Logic #Math #CompSci #FunctionalProgramming #Haskell
• #Exercitium: Sucesión de números amigos. #Haskell #Python #Matemáticas
• #Exercitium: Suma de los números amigos menores que n. #Haskell #Python #Matemáticas
• Game "An introduction to constructive logic". ~ Mark Fischer et als./#/g/trequetrum/lean4game-logic #ITP #LeanProver #Logic
• Vertex algebras in Mathlib: coming soon? ~ Scott Carnahan. #ITP #LeanProver #Math
• Real world autoformalization. ~ Siddhartha Gadgil. #ITP #LeanProver #Math
• Building a formal verification framework for smart contracts. ~ Jakob von Raumer. #ITP #LeanProver
• 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 #LeanProver #AI
• Information theory in Lean: the DPI. ~ Lorenzo Luccioli. #ITP #LeanProver
• A nimble introduction to nimbers. ~ Violeta Hernández Palacios. #ITP #LeanProver #Math
• An agda2hs-compatible representation of exact real arithmetic. ~ Viktor Csimma. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating SAT and SMT solvers on large-scale sudoku puzzles. ~ Liam Davis, Tairan Ji. #SAT #SMT
• The Haskell Unfolder Episode 38: tasting and testing CUDA (map, fold, scan). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• U-MATH: A university-level benchmark for evaluating mathematical skills in LLMs. ~ Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, Alex Myasnikov, Vlad Stepanov, Alexei Miasnikov, Sergei Tilga. #LLMs #Math

The readings shared in Bluesky on 15 January 2025 are

• Readings shared January 14, 2025. #ITP #IsabelleHOL #Coq #Rocq #Haskell #FunctionalProgramming
• #Exercitium: Sucesión de números amigos. #Haskell #Matemáticas
• Root systems and root data in Mathlib. ~ Oliver Nash. #ITP #LeanProver
• An introduction to linters. ~ Damiano Testa. #ITP #LeanProver
• Efficient forward reasoning for Aesop. ~ Xavier Généreux, Jannis Limperg. #ITP #LeanProver
• The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory. ~ Emily Riehl. #ITP #LeanProver
• Searching for proof improvements with tryAtEachStep. ~ David Renshaw. #ITP #LeanProver
• From Aristotle to the iPhone. ~ Moshe Vardi. #Logic #Math #CompSci

The readings shared in Bluesky on 14 January 2025 are

• Readings shared January 13, 2025. #ITP #Coq #Rocq #HOL4 #CommonLisp #Programming #Math
• An Isabelle/HOL framework for synthetic completeness proofs. ~ Asta Halkjær From. #ITP #IsabelleHOL
• An Isabelle formalization of co-rewrite pairs for non-reachability in term rewriting. ~ Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL
• Formalizing simultaneous critical pairs for confluence of left-linear rewrite systems. ~ Christina Kirk, Aart Middeldorp. #ITP #IsabelleHOL
• Formalized Burrows-Wheeler transform. ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #ITP #IsabelleHOL
• Formalizing the one-way to hiding theorem. ~ Katharina Heidler, Dominique Unruh. #ITP #IsabelleHOL
• Further tackling Post correspondence problem and proof generation. ~ Akihiro Omori, Yasuhiko Minamide. #ITP #IsabelleHOL
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq #Rocq
• Hell (Haskell shell): Year in review. ~ Chris Done. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 13 January 2025 are

• Readings shared January 12, 2025. #ITP #Coq #Rocq #Math #HoTT #CommonLisp #LogicProgramming #Prolog #LPTP
• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Rocq
• Coinductive proofs for temporal hyperliveness. ~ Arthur Correnson, Bernd Finkbeiner. #ITP #Coq #Rocq
• Reversible computation with stacks and "Reversible management of failures". ~ Matteo Palazzo, Luca Roversi. #ITP #Coq #Rocq
• Preservation of speculative constant-time by compilation. ~ Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte. #ITP #Coq #Rocq
• Proof recommendation system for the HOL4 theorem prover. ~ Nour Dekhil, Adnan Rashid, Sofiene Tahar. #ITP #HOL4
• The way of Lisp or the right thing. ~ Joe Marshall. #CommonLisp #Programming
• A road to Common Lisp. ~ Steve Losh (2018). #CommonLisp
• cl-digraph: an implementation of a mutable directed graph data structure for Common Lisp. ~ Steve Losh. #CommonLisp #Math

The readings shared in Bluesky on 12 January 2025 are

• Readings shared January 11, 2025. #ITP #LeanProver #Coq #Rocq #Agda #FunctionalProgramming #Haskell #Python #Math #CategoryTheory #ComputerSci #Education #GenAI
• Prouver que π est irrationnel avec MathComp-Analysis. ~ Reynald Affeldt. #ITP #Coq #Rocq #Math
• Reconciling impredicative axiom and universe. ~ Stefan Monnier. #ITP #Coq #Rocq #HoTT
• Vers une automatisation de la certification des propriétés de clôture pour Prolog. ~ Thierry Marianne, Fred Mesnard, Etienne Payet. #Prolog #LogicProgramming #LPTP
• Why I chose Common Lisp. ~ Dan's Musings. #CommonLisp
• Common Lisp community survey 2024 results. ~ Dan Haskin. #CommonLisp
• Common Lisp. #CommonLisp

The readings shared in Bluesky on 11 January 2025 are

• Readings shared January 10, 2025. #ITP #LeanProver #Logic #Math #Haskell #Python #ASP #LogicProgramming #AI #NeuroSymbolicAI #LLMs
• #Exercitium: Números amigos. #Haskell #Python #Matemáticas
• Categories and Haskell (An introduction to the mathematics behind modern functional programming). ~ Jan-Willem Buurlage. #CategoryTheory #Haskell #FunctionalProgramming
• LeanUniverse: A library for consistent and scalable Lean4 dataset management. ~ Aram H. Markosyan, Gabriel Synnaeve, Hugh Leather. #ITP #LeanProver
• Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre Corbineau, Basile Gros, Jean-François Monin. #ITP #Coq #Rocq
• On the correctness of Barron and Strachey’s cartesian product function. ~ Wouter Swierstra, Jason Hemann. #Haskell #FunctionalProgramming #ITP #Agda
• Alpha beta pruning with the selection monad. ~ Johannes Hartmann, Jeremy Gibbons. #Haskell #FunctionalProgramming
• Using GHC core to normalise student programs. ~ Matilda Blomqvist, Alex Gerdes. #Haskell #FunctionalProgramming
• Shallowly embedded functions. ~ Mart Lubbers, Pieter Koopman, Niek Janssen. #Haskell #FunctionalProgramming
• CoScheme: Compositional copatterns in Scheme. ~ Paul Downen, Adriano Corbelino II. #FunctionalProgramming
• Assessment in computer science education in the GenAI era (Prioritizing critical thinking over syntax mastery). ~ Orit Hazzan. #ComputerSci #Education #GenAI

The readings shared in Bluesky on 10 January 2025 are

• Readings shared January 9, 2025. #ITP #LeanProver #Logic #Math #FunctionalProgramming #Haskell #JavaScript #Python #AI #NeuralNetwork #ChatGPT
• #Exercitium: Máxima suma de caminos en un triángulo. #Haskell #Python #Matemáticas
• Teaching "Foundations of mathematics" with the LEAN theorem prover (Master's Thesis). #ITP #LeanProver #Logic #Math
• Learning to automatically solve logic grid puzzles. ~ Arindam Mitra, Chitta Baral (2015). #ASP #LogicProgramming
• Neuro-symbolic AI in 2024: A systematic review. ~ Brandon C. Colelough, William Regli. #AI #NeuroSymbolicAI
• Un comparador de modelos de Inteligencia Artificial. ~ @Alvy. #AI #LLMs

The readings shared in Bluesky on 9 January 2025 are

• Readings shared January 8, 2025. #ITP #IsabelleHOL #AI #MachineLearning #LLMs
• Teaching "Foundations of mathematics" with the LEAN theorem prover. ~ Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Using a JavaScript component inside a Haskell application. ~ Mateusz Goślinowski. #Haskell #FunctionalProgramming #JavaScript
• Mathematics of neural networks (Lecture notes graduate course). ~ Bart M.N. Smets. #NeuralNetwork #Math
• Notes on mathematical logic (Vol. 1). ~ David W. Kueker. #Logic #Math
• Notes on mathematical logic (Vol. 2). ~ David W. Kueker. #Logic #Math
• ChatGPT: Cómo hacer (y mejorar) mi Trabajo de Fin de Carrera de la Universidad en un par de minutos. ~ Chema Alonso. #ChatGPT #Python #Programming

The readings shared in Bluesky on 8 January 2025 are

• Readings shared January 6, 2025. #ITP #IsabelleHOL #LeanProver #Lean4 #Agda #Coq #Rocq #HoTT #Math #AI #LLMs
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• Can AI models reason like a human? ~ Wayne Joubert. #AI #LLMs
• Artificial intelligence then and now (From engines of logic to engines of bullshit?). ~ Thomas Haigh. #AI #MachineLearning #LLMs

The readings shared in Bluesky on 6 January 2025 are

• Readings shared January 4, 2025. #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python
• Computing huge Fibonacci numbers, by proof and by code. ~ Lawrence Paulson. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #LeanProver #Lean4 #Math
• Mathematicians found – and fixed – an error in a 60-year-old proof. ~ Alex Wilkins.L#selection-733.0-733.66 #ITP #LeanProver #Math
• Large language models for mathematical analysis. ~ Ziye Chen, Hao Qi. #AI #LLMs #Math
• On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. #ITP #Agda #HoTT
• Laws of quantum programming. ~ Mingsheng Ying, Li Zhou, Gilles Barthe. #ITP #Coq #Rocq #QuantumProgramming
• El libro recursivo de la recursividad. ~ @Alvy. #Programación

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 2, 2025. #Haskell #Python #Math
• #Exercitium: Mayor órbita de la sucesión de Collatz. #Haskell #Python #Matemáticas
• Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Décomposition algébrique cylindrique en Coq/Rocq. ~ Quentin Vermande. #ITP #Coq #Rocq #Math
• Formalizing adhesive category theory in Rocq. ~ Samuel Arsac, Russell Harmer, Damien Pous. #ITP #Rocq
• Vérification de bout en bout d’une fonction de bibliothèque mathématique. ~ Paul Geneau de Lamarlière. #ITP #Coq #Rocq #Math
• Safe external calls from formally verified functional code: exiting the monad, and a BDD case study. ~ David Monniaux, Sylvain Boulmé. #ITP #Coq #Rocq
• Modular probabilistic programming with algebraic effects. ~ Oliver Goldstein, Ohad Kammar. #Haskell #FunctionalProgramming
• Parallel QuickHull algorithm in Haskell. ~ George Morgulis, Henry Lin. #Haskell #FunctionalProgramming
• Parallel SAT solver. ~ Yixuan Li, Jiaqian Li, Phoebe Wang. #Haskell #FunctionalProgramming
• Storable types: free, absorbing, custom. ~ Basile Clément, Camille Noûs, Gabriel Scherer. #OCaml #FunctionalProgramming
• Typechecking of overloading in programming languages and mechanized mathematics. ~ Arthur Charguéraud, Martin Bodin, Louis Riboulet. #OCaml #FunctionalProgramming
• Applying machine learning to number-theoretical data (A focus on class groups of imaginary quadratic fields). ~ Hugo Sträng. #AI #MachineLearning #Math

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 3, 2025. #ITP #Lean4 #IsabelleHOL #Coq #Rocq #Math #FunctionalProgramming #OCaml #Haskell #Python #AI #MachineLearning
• #Exercitium: Caminos en un triángulo. #Haskell #Python #Matemáticas
• Demostraciones con Isabelle/HOL del "Praeclarum theorema" de Leibniz. #ITP #IsabelleHOL #Logic
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als.. #ITP #LeanProver #Math
• Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. #ITP #HOL_Light #Logic
• Ascoli-Arzel`a theorem (Metric space version). ~ Keiichi Miyajima, Hiroshi Yamazaki. #ITP #Mizar #Math
• Universality of measure space. ~ Noboru Endou, Yasunari Shidama. #ITP #Mizar #Math
• Formalization of orthogonal complements of normed spaces. ~ Hiroyuki Okazaki. #ITP #Mizar #Math

The readings shared in Bluesky on 2 January 2025 are

• Readings shared January 1, 2025. #ITP #LeanProver #Lean4 #Mizar #Math #Haskell #Python
• #Exercitium: Ternas pitagóricas con suma dada. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 1 January 2025 are

• Readings shared December 31, 2024. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Formal proof of transcendence of the number e (Part I). ~ Yasushige Watase. #ITP #Mizar #Math
• Formal proof of transcendence of the number e (Part II). ~ Yasushige Watase. #ITP #Mizar #Math
• #Exercitium: Suma de múltiplos de 3 o de 5. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 31 December 2024 are

• Readings shared December 30, 2024. #ITP #Coq #Rocq #FunctionalProgramming #Haskell #CommonLisp #EmacsLisp #Emacs #Logic #Math #CategoryTheory #AI
• A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL

The readings shared in Bluesky on 30 December 2024 are

• Readings shared December 29, 2024. #Haskell #Python #Math #AI #ITP
• Formal verification of a custom scheduling algorithm and specification of a Round-Robin implementation using Coq. ~ Christian Choa et als. #ITP #Coq #Rocq
• Formal verification of shortest job first scheduling algorithm in Coq. ~ Jian Lawrence Luteria et als. #ITP #Coq #Rocq
• Rocq prover: A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more. #ITP #Rocq
• Generalized Dijkstra in Haskell. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Tutorial on good Lisp programming style. ~ Peter Norvig, Kent Pitman (1993). #CommonLisp #Programming
• Paradigms of artificial intelligence programming (Case studies in Common Lisp). ~ Peter Norvig. #eBook #AI #CommonLisp #Programming
• Emacs Lisp guide. ~ Chris Done. #Emacs #Lisp
• Category theory illustrated. ~ Jencel Panic. #CategoryTheory
• Mathematical expression and reasoning for computer science. ~ David Liu, Toniann Pitassi. #eBook #Logic #Math #CompSci
• How to use Emacs as a desktop environment in Linux with EXWM. ~ Ramces Red. #Emacs
• Historias de la IA: los autómatas. ~ Manuel de León. #IA #Autómatas

The readings shared in Bluesky on 29 December 2024 are

• Readings shared December 27, 2024. #ITP #IsabelleHOL #Math #Teaching #AI #LLMs #Emacs
• #Exercitium: Exponente en la factorización. #Haskell #Python #Matemáticas
• Machine-assisted proof. ~ Terence Tao. #Math #AI #ITP
• AMS Advisory Group on Artificial Intelligence. ~ Akshay Venkatesh, Mark C. Wilson. #Math #AI

The readings shared in Bluesky on 27 December 2024 are

• Readings shared December 26, 2024. #Haskell #Python #Math
• A generalization of the Cauchy–Davenport theorem (in Isabelle/HOL). ~ Mantas Bakšys. #ITP #IsabelleHOL #Math
• Formally verified approximate policy iteration. ~ Maximilian Schäffeler, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Myths of mathematics teaching. ~ Daniel J. Velleman. #Math #Teaching
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. #AI #LLMs #Math
• AI: Beyond the headlines (The hype surrounding artificial intelligence has created misconceptions that may lead to missed opportunities). ~ Erdin Beshimov. #AI
• Dibujando figuras con Emacs. ~ Notxor. #Emacs

The readings shared in Bluesky on 26 December 2024 are

• Readings shared December 25, 2024. #Haskell #Python #Math #ITP #LeanProver #Lean4 #Lisp #Programming
• #Exercitium: Reconocimiento de potencias de 4. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 25 December 2024 are

• Readings shared December 24, 2024. #ITP #Agda #Haskell #FunctionalProgramming #Haskell #Python #AI #LLMs #Math
• #Exercitium: El teorema de Navidad de Fermat. #Haskell #Python #Math
• Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• The bipolar Lisp programmer. ~ Mark Tarver. #Lisp #Programming

The readings shared in Bluesky on 24 December 2024 are

• Readings shared December 23, 2024. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization #Programming #JuliaLang #Python #MachineLearning #Golog #LogicProgramming
• #Exercitium: Producto de los elementos de la diagonal principal. #Haskell #Python #Matemáticas
• Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. #ITP #Math #Education
• Data for mathematical copilots: Better ways of presenting proofs for machine learning. ~ Simon Frieder et als. #AI #LLMs #Math
• Compiling dependent type preconditions to runtime checks with Agda2Hs. ~ Jakob Naucke. #ITP #Agda #Haskell #FunctionalProgramming

The readings shared in Bluesky on 23 December 2024 are

• Readings shared December 21, 2024. #ITP #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization
• Can AI do maths yet? Thoughts from a mathematician. ~ Kevin Buzzard. #AI #ITP #Math
• The state of Julia for scientific machine learning. ~ Edward Berman, Jacob Ginesin. #Programming #JuliaLang #Python #MachineLearning
• LTLf synthesis on first-order agent programs in nondeterministic environments. ~ Till Hofmann, Jens Claßen. #AI #Golog #LogicProgramming

The readings shared in Bluesky on 21 December 2024 are

• Readings shared December 20, 2024. #ITP #Mizar #Math #Haskell #Python #AI
• Isabelle quick start guide. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• An imperative programmer tries to learn Haskell. ~ Thane Thomson. #Haskell #FunctionalProgramming
• Solving perfect numbers quickly with Haskell. ~ Andrew MacGillivray. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 20 December 2024 are

• Readings shared December 19, 2024. #ITP #IsabelleHOL #Mizar #Logic #Math #Haskell #FunctionalProgramming #LLMs
• #Exercitium: Reiteración de suma de consecutivos. #Haskell #Python #Matemáticas
• Formalize the octonions. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Apriori knowledge in an era of computational opacity: The role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math

The readings shared in Bluesky on 19 December 2024 are

• Readings shared December 18, 2024. #ITP #Agda #Mizar #Math #AI
• A formalization of sequent calculus for classical implicational logic. ~ Frederik Krogsdal Jacobsen, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• Elementary number theory problems (Part XV – Diophantine equations). ~ Karol Pąk, Artur Korniłowicz. #ITP #Mizar #Math
• Linear calculi: A comparison approach. ~ Ana Jorge Carvalho de Soares Almeida. #Haskell #FunctionalProgramming
• A survey of mathematical reasoning in the era of multimodal large language model: Benchmark, method & challenges. ~ Yibo Yan et als. #LLMs #Math #Reasoning

The readings shared in Bluesky on 18 December 2024 are

• Readings shared December 16, 2024. #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math
• Intrinsic verification of parsers and formal grammar theory in dependent Lambek calculus. ~ Steven Schaefer et als. #ITP #Agda
• Proofs in the Wild. ~ Mike Dodds. #ITP #AI
• Loops in Mizar. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Artificial intelligence: Principles and practice. ~ George F. Luger. #AI

The readings shared in Bluesky on 16 December 2024 are

• Readings shared December 15, 2024. #Haskell #FunctionalProgramming #CategoryTheory #AI #ITP #LeanProver #Math
• Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• Bottom-up computation using trees of sublists. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
• 'Lean-style' tactics in Knuckledragger. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• An example of goal-directed, calculational proof. ~ Roland Carl Backhouse, Walter Guttmann, Michael Winter. #Logic
• Pascal Costanza's Highly Opinionated Guide to Lisp. ~ Pascal Costanza. #CommonLisp #Programming
• Proposing and solving olympiad geometry with guided tree search. ~ Chi Zhang et als. #AI #Math

The readings shared in Bluesky on 15 December 2024 are

• Readings shared December 13, 2024. #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #Haskell #FunctionalProgramming #CategoryTheory
• The future of Math with o1 reasoning with Terence Tao, Mark Chen, and James Donovan. #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 13 December 2024 are

• Readings shared December 12, 2024. #ITP #LeanLang #Lean4 #Math
• On extending incorrectness logic with backwards reasoning. ~ Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran. #ITP #IsabelleHOL
• Machine checked proofs and programs in algebraic combinatorics. ~ Florent Hivert. #ITP #Coq #Rocq #Math
• Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. #ATP #Prover9 #Mace4 #Logic #Math

The readings shared in Bluesky on 12 December 2024 are

• Readings shared December 11, 2024. #ITP #IsabelleHOL #Logic #Math #SetTheory #Haskell #FunctionalProgramming
• Fermat’s Last Theorem — how it’s going. ~ Kevin Buzzard. #ITP #LeanLang #Lean4 #Math

The readings shared in Bluesky on 11 December 2024 are

• Readings shared December 10, 2024. #Haskell #Python #Math #Logic #SMT #Z3 #Python #LLMs #Prolog #LogicProgramming
• Isomorphic transfer infrastructure for nested types in Isabelle/HOL (Work in progress). ~ Gergely Buday, Andrei Popescu. #ITP #IsabelleHOL
• When is a call stack not a call stack? ~ Chris Smith. #Haskell #FunctionalProgramming
• Gödel's program in set theory. ~ Sandra Müller, Grigor Sargsyan. #Logic #Math #SetTheory
• Constructive theory of ordinals. ~ Thierry Coquand, Henri Lombardi, Stefan Neuwirth. #Logic #Math #SetTheory

The readings shared in Bluesky on 10 December 2024 are

• Readings shared December 9, 2024. #ITP #LeanLang #Lean4 #Haskell #FunctionalProgramming
• #Exercitium: Suma fila del triángulo de los impares. #Haskell #Python #Matemáticas
• Dyckhoff intuitionistic propositional prover. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• Enhancing mathematical reasoning in LLMs with background operators. ~ Jiajun Chen, Yik-Cheung Tam. #LLMs #Prolog #LogicProgramming

The readings shared in Bluesky on 9 December 2024 are

• Readings shared December 8, 2024. #ITP #Agda #Coq #Haskell #FunctionalProgramming
• Information sign: Search and coupling (Metavariables, coupling, and formal proofs). ~ Leni Aniva. #ITP #LeanLang #Lean4
• Debugging your Haskell application with debuggable. ~ Edsko de Vries. #Haskell #FunctionalProgramming
• Myth and truth in Haskell asynchronous exceptions. ~ Kazu Yamamoto. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 8 December 2024 are

• Readings shared December 6, 2024. #Haskell #FunctionalProgramming #AI #LLMs #ITP #Math
• Gradual guarantee via step-indexed logical relations in Agda. ~ Jeremy G. Siek. #ITP #Agda
• Explicit weakening. ~ Philip Wadler. #ITP #Agda
• Formally verified hardening of C programs against hardware fault injection. ~ Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet. #ITP #Coq
• Efficient, portable, census-polymorphic choreographic programming. ~ Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 6 December 2024 are

• Readings shared December 5, 2024. #ITP #LeanLang #Lean4 #Coq #Rocq #IsabelleHOL #Logic #Math #FunctionalProgramming #Haskell #OCaml #AI #LLMs
• You could have invented Fenwick trees. ~ Brent A. Yorgey. #Haskell #FunctionalProgramming
• AI for Math fund. ~ Terence Tao. #AI #ITP #Math
• (Re)imagining mathematics in a world of reasoning machines. ~ Akshay Venkatesh. #Math #ITP #AI
• On program synthesis and Large Language Models (Why it is unlikely new developments in machine intelligence will eventually make programming obsolete). ~ Hans Hüttel. #AI #LLMs #Programming
• Pourquoi existe-t-il de nombreux paradigmes de programmation? ~ Oscar Plaisant, Max Lemoine. #Programming #CompSci

The readings shared in Bluesky on 5 December 2024 are

• Readings shared December 4, 2024. #ITP #LeanLang #Logic #Math
• Lean: First steps (18 - Our Own Definition). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• QuickSub: Efficient iso-recursive subtyping. ~ Litao Zhou, Bruno C.D.S. Oliveira. #ITP #Coq #Rocq
• Tail modulo cons, OCaml, and relational separation logic. ~ Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer. #ITP #Coq #OCaml #FunctionalProgramming
• The tensor product on Hilbert spaces (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL #Math
• The Haskell Unfolder Episode 37: Solving Advent of Code 2024 day 4. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems. ~ Roozbeh Yousefzadeh, Xuenan Cao. #LLMs #ITP #LeanLang #Lean4 #Math
• Amplifying human performance in combinatorial competitive programming. ~ Petar Veličković, Alex Vitvitskyi, Larisa Markeeva, Borja Ibarz, Lars Buesing, Matej Balog, Alexander Novikov. #AI #LLMs #Math
• OnlineProver: First experience with teaching formal proofs. ~ Joachim Kristensen et als. #Logic #Teaching

The readings shared in Bluesky on 4 December 2024 are

• Readings shared December 3, 2024. #ITP #LeanLang #IsabelleHOL #Coq #Rocq #Math #LLMs #ChatGPT
• Verified foundations for differential privacy. ~ Markus de Medeiros et als. #ITP #LeanLang
• Logic and linear algebra: An introduction. ~ Daniel Murfet. #Logic #Math

The readings shared in Bluesky on 3 December 2024 are

• Readings shared December 2, 2024. #ITP #LeanLang #Math #Calculemus #CategoryTheory #Math #Racket #FunctionalProgramming
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• All your base are belong to U^s (Sort polymorphism for proof assistants). ~ Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter. #ITP #CoqLang #Rocq
• Mechanised safety verification for a distributed autonomous railway control system. ~ Robert Sachtleben, Anne Haxthausen, Jan Peleska. #ITP #IsabelleHOL
• The mathematician who—incidentally—helped mathematicians to stop worrying and love the computer. ~ Keith Devlin. #Math
• ChatGPT turns two: how the AI chatbot has changed scientists’ lives (How many researchers are using the AI tool? Nature gathers data and talks to members of the academic community). ~ Mariana Lenharo. #LLMs #ChatGPT

The readings shared in Bluesky on 2 December 2024 are

• Readings shared December 1, 2024. #ITP #IsabelleHOL #Math
• Proofs of "If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab" in Lean4. #ITP #Lean4 #Math #Calculemus
• Lean: First steps (15 - Zero product). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (16 - Writing our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Category theory in programming. ~ Noah Ma. #CategoryTheory #Math #Racket #FunctionalProgramming

The readings shared in Bluesky on 1 December 2024 are

• Readings shared November 30, 2024. #Lean4 #FunctionalProgramming
• The sum-of-squares function and Jacobi's two-square theorem (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math

The readings shared in Bluesky on 30 November 2024 are

• Readings shared November 29, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Calculemus #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry #Haskell #FunctionalProgramming #Programming #FormalVerification #Dafny
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #Lean4 #FunctionalProgramming

The readings shared in Bluesky on 29 November 2024 are

• Readings shared November 28, 2024. #ITP #IsabelleHOL #Logic #Math #Haskell #FunctionalProgramming
• Proof of "If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac" in Lean4. #ITP #Lean4 #Math #Calculemus
• Machine learning and mathematics (The twin catalysts poised to accelerate twenty-first century mathematics: formalisation and machine learning). ~ Harald Carlens. #Math #ITP #Lean4 #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry
• Deep embedding of intuitionistic linear logic. ~ Filip Smola, Jacques D. Fleuriot. #ITP #IsabelleHOL #Logic #Math
• Brillo: Painless 2D vector graphics, animations, and simulations powered by GLFW (Fork of gloss). ~ Adrian Sieber. #Haskell #FunctionalProgramming
• Effectiveness of Large Language Models to generate formally verified C code. ~ Merlijn Sevenhuijsen. #LLMs #Programming #FormalVerification
• dafny-annotator: AI-assisted verification of Dafny programs. ~ Gabriel Poesia, Chloe Loughridge, Nada Amin. #LLMs #Dafny #FormalVerification

The readings shared in Bluesky on 28 November 2024 are

• Readings shared November 27, 2024. #Haskell #FunctionalProgramming #AI #MachineLearning #Math
• Semantics for linear-time temporal logic with finite observations. ~ Rayhana Amjad, Rob van Glabbeek, Liam O'Connor. #ITP #IsabelleHOL #Logic #Math
• Competitive Programming in Haskell: stacks, queues, and monoidal sliding windows. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 27 November 2024 are

• Readings shared November 26, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Prolog #LogicProgramming #Z3 #SMT #AI #Education
• Haskell: A great procedural language. ~ kqr. #Haskell #FunctionalProgramming
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #Haskell #FunctionalProgramming
• Linear algebra done right. ~ Sheldon Axler. #eBook #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper, Anibal M. Medina-Mardones, Bartłomiej Lewandowski, Angus Gruen, Piotr Kucharski, Sergei Gukov. #AI #MachineLearning #Math

The readings shared in Mastodon on 26 November 2024 are

• Readings shared November 25, 2024. #ITP #Lean4 #Rocq #FunctionalProgramming #CommonLisp
• Impossibility of the dissection of a cube (in Isabelle/HOL). ~ Thomas Holme Surlykke. #ITP #IsabelleHOL #Math
• Two theorems on hermitian matrices (in Isabelle/HOL). ~ Sage Binder, Zilin Jiang. #ITP #IsabelleHOL #Math
• Ground lambda Prolog. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl. ~ Stefan Neuwirth, Henri Lombardi, Thierry Coquand. #Logic #Math
• Grupos y capturas reemplazando texto con expresiones regulares. ~ Fernando Briano. #Emacs
• Lean: First steps (18 - Our own definition). ~ Tariq Rashid. #ITP #Lean4 #Math
• IA Generativa: Estrategias de uso para docentes desde infantil a bachillerato. ~ Pablo Haya. #AI #Education

The readings shared in Mastodon on 25 November 2024 are

• Readings shared November 24, 2024. #ITP #Lean4 #Math #AI #LLMs #Programming #Education
• Cryptography experiments in Lean 4: SHA-3 implementation. ~ Gérald Doussot. #ITP #Lean4 #FunctionalProgramming
• Scaling up mechanized proof automation for small-step semantics. ~ Sandrine Blazy, Alain Delaët, Denis Merigoux. #ITP #Rocq
• Counting connected components of a graph. ~ Atabey Kaygun. #FunctionalProgramming #CommonLisp

The readings shared in Mastodon on 24 November 2024 are

• Readings shared November 23, 2024. #Math #SetTheory #Bluesky
• Lean: First steps (Appendix B - Libraries). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Papers with computer-checked proofs. ~ Daniel J. Bernstein. #ITP
• Does AI mean the end of teaching programming? ~ Alfred Thompson. #AI #Programming #Education
• Are Large Language Models memorizing bug benchmarks? ~ Daniel Ramos, Claudia Mamede, Kush Jain, Paulo Canelas, Catarina Gamboa, Claire Le Goues. #LLMs #Programming

The readings shared in Mastodon on 23 November 2024 are

• Readings shared November 22, 2024. #Logic #Math #FCA #ConExp #AI
• 'A place of joy': why scientists are joining the rush to Bluesky. ~ Smriti Mallapaty. #Bluesky
• Axiomatic set theory (Version of 23 November 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on 22 November 2024 are

• Readings shared November 21, 2024. #ITP #Lean4 #Coq #Haskell #OCaml #FunctionalProgramming #ITP #Prolog #LogicProgramming #Math
• The elementary theory of free Steiner triple systems. ~ Silvia Barbina, Enrique Casanovas. #Logic #Math
• FCA (Formal Concept Analysis) using the Concept Explorer in 2024. ~ Edith Vargas-GarcÍa, Andreas Wachtel. #FCA #ConExp
• Conferencia Leonardo Torres Quevedo: ¿Puede pensar una máquina? ~ Francisco A. González Redondo y Alfonso Hernando González. #AI

The readings shared in Mastodon on 21 November 2024 are

• Readings shared November 20, 2024. #ITP #Lean4 #Math #AI
• Lean4 and the Curry-Howard isomorphism. ~ Luis Wirth. #ITP #Lean4
• Repository for the conference "Lean For The Curious Mathematician 2024". #ITP #Lean4 #Math
• The denotational semantics of SSA. ~ Jad Elkhaleq Ghalayini, Neel Krishnaswami. #ITP #Lean4
• Tail modulo cons, OCaml, and relational separation logic. ~ Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer. #ITP #Coq #OCaml #FunctionalProgramming
• Scientific computing with confidence using typed dimensions. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 36: Concurrency and the FFI. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Prolog Trinity ecosystem (Extracts from the current manuscripts). ~ Torbjörn Lager. #Prolog #LogicProgramming
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #Prolog #LogicProgramming

The readings shared in Mastodon on 20 November 2024 are

• Readings shared November 19, 2024. #ITP #Lean4 #Math #Haskell #FunctionalProgramming
• Anatomy of a formal proof. ~ Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz. #ITP #Lean4 #Math
• A course of Algebra (Part I). ~ Aleksandr Aleksandrovich Zykov. #Math
• El aprendizaje automático ayuda a atacar problemas matemáticos clásicos. ~ Juanjo Rué y Ágata A. Timón. #AI #Math

The readings shared in Mastodon on 19 November 2024 are

• Readings shared November 18, 2024. #LLMs #Math #Reasoning #Logic #TypeTheory
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Competitive programming in Haskell: Union-Find, part II. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 18 November 2024 are

• Readings shared November 17, 2024. #ITP #Coq #Haskell #CommonLisp #FunctionalProgramming #Python #Programming #CategoryTheory
• Do Large Language Models truly grasp mathematics? An empirical exploration from cognitive psychology. ~ Wei Xie, Shuoyoucheng Ma, Zhenhua Wang, Enze Wang, Kai Chen, Xiaobing Sun, Baosheng Wang. #LLMs #Math #Reasoning
• Monoid theory in Alonzo: A little theories formalization in simple type theory. ~ William M. Farmer, Dennis Y. Zvigelsky. #Logic #Math #TypeTheory

The readings shared in Mastodon on 17 November 2024 are

• Readings shared November 16, 2024. #ITP #Lean4 #FunctionalProgramming #Math #AI #LLMs #Git #GitHub
• Designing proof deautomation for Coq. ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Andrew Head, Benjamin C. Pierce. #ITP #Coq
• Type-checking and type-inference. ~ René Thiemann. #Haskell #FunctionalProgramming
• Type-inference in Haskell, kinds and explicit foralls. ~ René Thiemann. #Haskell #FunctionalProgramming
• Functors, record syntax, case study: a simple parser. ~ René Thiemann. #Haskell #FunctionalProgramming
• Monads in general, state monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Evaluation of monadic code, example: Tseitin, error monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Parsing in general, Parsec. ~ René Thiemann. #Haskell #FunctionalProgramming
• Number of isomorphism classes of ternary trees. ~ Atabey Kaygun. #FunctionalProgramming #CommonLisp
• Sieves and sheaves. ~ Bartosz Milewski. #CategoryTheory
• Python is no more the king of data science (5 reasons why Python is losing its crown). ~ Abdur Rahman. #Python #Programming

The readings shared in Mastodon on 16 November 2024 are

• Readings shared November 15, 2024. #ITP #LeanProver #Math #SetTheory #Haskell #FunctionalProgramming #AI #LLMs
• Code with proofs: The Arena. #ITP #Lean4 #FunctionalProgramming
• The Turing Test and our shifting conceptions of intelligence. ~ Melanie Mitchell. #AI
• Debates on the nature of artificial general intelligence. ~ Melanie Mitchell. #AI
• Large Language Models. ~ Melanie Mitchell. #AI #LLMs
• GitHub for mathematicians. ~ Steven Clontz. #Git #GitHub
• Code4math: Consortium of Digital Ecosystems for Mathematics. #Math

The readings shared in Mastodon on 15 November 2024 are

• Readings shared November 14, 2024. #ITP #LeanProver #Coq #ATP #Logic #Math #Haskell #FunctionalProgramming #FormalMethods #CompSci #Education #RustLang #AI #LLMs
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• The Haskell inlining and specialization FAQ. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
• Axiomatic set theory (Version of 9 November 2024). ~ Tom Leinster. #Math #SetTheory
• The metaphors of artificial intelligence. ~ Melanie Mitchell. #AI #LLMs

The readings shared in Mastodon on 14 November 2024 are

• Readings shared November 13, 2024. #ITP #Lean4 #Math #Physics #ATP #SAT_Solvers
• VEL: A formally verified reasoner for ℰℒ++ description logic. ~ Atalay Mert Ileri1, Hande Küçük McGinty. #ITP #Coq #Logic
• La formalización automatizada de las matemática: Una historia de cómo la necesidad hizo la virtud. ~ David de Frutos Escrig. #ITP #LeanProver #Math
• Debugging Haskell type errors. ~ Tikhon Jelvis. #Haskell #FunctionalProgramming
• The role of formal methods in computer science education. ~ Maurice ter Beek, Manfred Broy, Brijesh Dongol. #FormalMethods #CompSci #Education
• Resolution prover in Rust. ~ Wanda Rosmus. #Logic #ATP #RustLang
• AI’s math problem: FrontierMath benchmark shows how far technology still has to go. ~ Michael Nuñez. #AI #Math
• A holistic and critical look at language agents. ~ Yu Su. #AI #LLMs

The readings shared in Mastodon on 13 November 2024 are

• Readings shared November 12, 2024. #ITP #LeanProver #LLMs #Emacs
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio, Adam Topaz. #ITP #Lean4 #Math
• Formalization of physics index notation in Lean 4. ~ Joseph Tooby-Smith. #ITP #Lean4 #Math #Physics
• How to discover short, shorter, and the shortest proofs of unsatisfiability: A branch-and-bound approach for resolution proof length minimization. ~ Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović. #ATP #SAT_Solvers

The readings shared in Mastodon on 12 November 2024 are

• Readings shared November 11, 2024. #ITP #LeanProver #Logic #Math #LLMs
• Benchmarking automated theorem proving with Large Language Models. ~ Vanessa Lama, Catherine Ma, Tirthankar Ghosal. #ITP #LeanProver #LLMs
• BC-Prover: Backward chaining prover for formal theorem proving. ~ Yuhang He et als. #ITP #LeanProver #LLMs
• Programación literaria en Emacs (1ª parte). ~ Nyan Max. #Emacs

The readings shared in Mastodon on 11 November 2024 are

• Readings shared November 10, 2024. #ITP #Lean4 #Logic #Math #TFM
• NL²PS: A natural language to Lean proofs system. ~ Yifan Luo, Kangping Xu.V#discussion #ITP #LeanProver #LLMs
• VCVio: A formally verified forking lemma and Fiat-Shamir transform, via a flexible and expressive oracle representation. ~ Devon Tuma, Nicholas Hopper. #ITP #LeanProver
• The art of proof (Basic training for deeper mathematics). ~ Matthias Beck, Ross Geoghegan. #Logic #Math

The readings shared in Mastodon on 10 November 2024 are

• Readings shared November 9, 2024. #ITP #Agda #Logic #Math #SetTheory #AI #MachineLearning
• #Calculemus: Proofs with Lean4 of "If u(n) tends to a, then 7u(n) tends to 7a". #ITP #Lean4 #Math
• An introduction to mathematical proof. ~ Seçkin Demirbaş, Andrew Rechnitzer, Hannah Kohut. #Logic #Math
• Los números metálicos. ~ Marta Macho Stadler. #Math
• Los números vistos como bosques. ~ Marta Macho Stadler. #Math
• Problemas de competición sobre combinatoria. ~ Araceli Arjona Muñoz. #TFM #Math
• Problemas de probabilidad de Olimpiada Matemática. ~ Eduardo Cebrián García. #TFM #Matemáticas
• Análisis y resolución de problemas sobre desigualdades numéricas en la preparación de la Olimpiada de Matemáticas. ~ Sara Amaro Serrano. #TFM #Matemáticas
• Análisis y resolución de problemas sobre teoría de juegos. ~ Celia García Ruiz. #TFM #Matemáticas
• Invariantes en la resolución de problemas. ~ José Félix Sánchez Martínez. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Aritmética. ~ Inmaculada Perálvarez Bermúdez. #TFM #Matemáticas
• Problemas de olimpiadas sobre números complejos. ~ Paola Posadas Prados. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Ecuaciones diofánticas. ~ Antonio Manuel Ortega Torres. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Desigualdades. ~ Iván Valero Terrón. #TFM #Matemáticas
• Problemas de Olimpíadas Matemáticas sobre Probabilidad. ~ Marta Fernández Rodríguez. #TFM #Matemáticas
• Problemas y aplicaciones de sucesiones recurrentes. ~ Carlos Cervera Zafra. #TFM #Matemáticas
• Estudio de problemas sobre ecuaciones funcionales en el nivel de Olimpiadas Matemáticas. ~ Luis Castro Castro. #TFM #Matemáticas
• Números curiosos. ~ Pascual Jara. #Matemáticas
• Paradojas. ~ Pascual Jara Martínez. #Lógica #Matemáticas
• Sucesiones recurrentes. ~ Pascual Jara Martínez. #Matemáticas

The readings shared in Mastodon on 9 November 2024 are

• Readings shared November 8, 2024. #Math #AI #LLMs #Math #Reasoning
• Formalising graph algorithms with coinduction. ~ Donnacha Oisín Kidney, Nicolas Wu. #ITP #Agda #Math
• Axiomatic set theory (Version of 3 November 2024). ~ Tom Leinster. #Math #SetTheory
• Introduction to mathematical proofs. ~ Shay Fuchs. #Logic #Math
• On the relevance of logic for AI, and the promise of neuro-symbolic learning. ~ Vaishak Belle. #Logic #AI #MachineLearning

The readings shared in Mastodon on 8 November 2024 are

• Readings shared November 7, 2024. #ITP #Coq #Lean4 #Agda #Logic #Math #Haskell #FunctionalProgramming #LLMs #ChatGPT #AI #Programming #Education
• Applications of graph theory. ~ Ashay Dharwadker, Shariefuddin Pirzada. #Math
• FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI. ~ Elliot Glazer et als. #AI #Math #Reasoning
• Benchmarking Large Language Models with integer sequence generation tasks. ~ Daniel O'Malley, Manish Bhattarai, Javier Santos. #AI #LLMs #Math

The readings shared in Mastodon on 7 November 2024 are

• Unification in matching logic — revisited. ~ Ádám Kurucz, Péter Bereczky, Dániel Horpácsi. #ITP #Coq
• Grupos en Lean. ~ Luis Turcio. #ITP #Lean4 #Math
• The Haskell Unfolder Episode 35: Distributive and representable functors. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What can we mean? (on practices, norms and pluralisms). ~ Greg Restall. #ITP #Agda #Lean #Logic #Math
• Learning rules explaining interactive theorem proving tactic prediction. ~ Liao Zhang, David M. Cerna, Cezary Kaliszyk. #ILP #ITP #Coq
• Next-token prediction task assumes optimal data ordering for LLM training in proof generation. ~ Chenyang An et als. #LLMs #ITP #LeanProver
• ChatGPT as tutor? A case study on competitive programming. ~ Juuso Rytilahti, Erno Lokkila. #ChatGPT #AI #Programming #Education

The readings shared in Mastodon on 5 November 2024 are

• Readings shared November 4, 2024. #ITP #Lean4 #Math
• Functors to Monads: A story of shapes. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 4 November 2024 are

• Readings shared November 3, 2024. #Haskell #FunctionalProgramming
• Lean: First steps (14 - Disequality again)​ (Video). ~ Tariq Rashid. #ITP #Lean4 #Math

The readings shared in Mastodon on 3 November 2024 are

• Readings shared November 2, 2024. #ITP #LeanProver #IsabelleHOL #Coq #Math #SetTheory #CategoryTheory #AI #LLMs #Autoformalization
• Competitive programming in Haskell: Union-find. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 2 November 2024 are

• Readings shared November 1, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #Haskell #FunctionalProgramming #Autoformalization #LLMs
• The future of Mathematics in a world of machines. ~ Simone Severini. #Math #ITP #LeanProver #AI #LLMs #Autoformalization
• AIPS: An Olympiad-level AI system for algebraic inequalities. #LLMs #ITP #Lean4 #Math
• Proving the existence of stable assignments in democratic forking using Isabelle/HOL. ~ Jan-Georg Smaus. #ITP #IsabelleHOL
• Verified parser- and printer-combinator bidefinition in the Isabelle proof assistant. ~ Matthias Sleurink. #ITP #IsabelleHOL
• The Boustrophedon transform, the Entringer numbers, and related sequences (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici, Nobuko Yoshida. #ITP #Coq
• Axiomatic set theory (Version of 31 October 2024). ~ Tom Leinster. #Math #SetTheory
• Basic category theory. ~ Tom Leinster. #Math #CategoryTheory
• Computational thinking: The idea that lived. ~ Shuchi Grover. #Education #Programming

The readings shared in Mastodon on 1 November 2024 are

• Readings shared October 31, 2024. #ITP #IsabelleHOL #Lean4 #Coq #Math #GenerativeAI
• Intuitionistic propositional logic in Lean. ~ Dafina Trufaş. #ITP #Lean4 #Logic #Math
• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #Coq #LLMs
• Going REPLing with Haskeline. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Proving Olympiad algebraic inequalities without human demonstrations. ~ Chenrui Wei, Mengzhou Sun, Wei Wang. #LLMs #ITP #Math
• Autoformalize mathematical statements by symbolic equivalence and semantic consistency. ~ Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma. #Autoformalization #LLMs #IsabelleHOL #Math

The readings shared in Mastodon on 31 October 2024 are

• Readings shared October 30, 2024. #ITP #Lean4 #IsabelleHOL #Math #ITP #Prolog #ASP #LogicProgramming #LambdaCalculus #AI #LLMs
• Lean: First steps (14 - Disequality again)​. ~ Tariq Rashid. #ITP #Lean4 #Math
• Babai’s nearest plane algorithm (in Isabelle/HOL). ~ Eric Ren, Sage Binder, Katherine Kosaian. #ITP #IsabelleHOL #Math
• Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math #Education
• Generative AI as an icebreaker to help us accept other ways of thinking. ~ Berry Billingsley, Ted Selker. #GenerativeAI
• The secret of Ramsey numbers (A new order forms out of randomness). ~ Chris Edwards. #Math #CompSci
• Ética, pensamiento crítico y responsabilidad en el uso de la IA en trabajos académicos (presentación). ~ Lluís Codina. #GenerativeAI #Education

The readings shared in Mastodon on 30 October 2024 are

• Readings shared October 29, 2024. #AI #XAI #LLMs #Logic #Reasoning #ASP #LogicProgramming
• Lean 4 tactic cheatsheet (October 29, 2024). ~ Floris van Doorn. #ITP #Lean4
• AI and Mathematics. ~ Terence Tao. #AI #Math #ITP #Lean4
• A formal characterization of discrete condensed objects. ~ Dagur Asgeirsson. #ITP #Lean4 #Math
• Minimal, maximal, least, and greatest elements w.r.t. restricted ordering (in Isabelle/HOL). ~ Martin Desharnais. #ITP #IsabelleHOL
• Programming with Math: The lambda calculus. #LambdaCalculus
• Prolog, Datalog, languages, resources, and beyond! #Prolog #ASP #LogicProgramming
• Combining logic with Large Language Models for automatic debugging and repair of ASP programs. ~ Ricardo Brancas, Vasco Manquinho, Ruben Martins. #ASP #LogicProgramming #LLMs

The readings shared in Mastodon on 29 October 2024 are

• Readings shared October 28, 2024. #ITP #Lean4 #Coq #Math #LLMs
• Tools are all you need. ~ Henry Kautz. #AI #LLMs #Logic #Reasoning
• Logic in the age of AI. ~ Yuri Gurevich. #Logic #AI
• Rigorous language models for trustworthy AI. ~ Yanhong A. Liu. #AI #LLMs #Logic #Reasoning
• Harnessing ASP and its extensions: Recent applications and role in Trustworthy AI. ~ Giuseppe Mazzotta, Francesco Ricca. #AI #ASP #LogicProgramming
• Advancements in xASP, an XAI system for Answer Set Programming. ~ Mario Alviano, Ly Ly Trieu, Tran Son, Marcello Balduccini. #ASP #XAI
• Logic-based explainability: Past, present & future. ~ Joao Marques-Silva. #XAI #Logic
• A case study on TSP: What to optimize and how? ~ Martin Gebser. #ASP #LogicProgramming
• Integrating reasoning systems for trustworthy AI (Proceedings of the 4th Workshop on Logic and Practice of Programming (LPOP)). ~ Anil Nerode, Yanhong A. Liu (eds.) #Logic #LogicProgramming #AI
• Combining LLM code generation with formal specifications and reactive program synthesis. ~ William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito. #LLMs
• Keynote presentation by Hal Abelson and Gerald Sussman at the fourteenth RacketCon: "Teaching people thinking: programming and powerful ideas" and "From computational thinking to computational action". #CompSci
• Introduction to Git and GitHub for Python developers. ~ Jim Anderson. #Git