The readings shared in Bluesky on 30 October 2025 are:

• Formalization of Auslander–Buchsbaum–Serre criterion in Lean4. ~ Naillin Guan, Yongle Hu. #ITP #LeanProver #Math
• Lists are geometric series. ~ iacgm. #Haskell #FunctionalProgramming
• #Exercitium: Rompecabeza matemático. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Distancia de Hamming. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 October 2025 are:

• Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #ITP #LeanProver #Math
• 1000+ theorems (The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!). ~ Katja Berčič et als. #Math #ITP #IsabelleHOL #HOL_Light #Rocq #LeanProver #Metamath #Mizar
• Combining textual and structural information for premise selection in Lean. ~ Job Petrovčič, David Eliecer Narvaez Denis, Ljupčo Todorovski. #AI #Math #ITP #LeanProver
• Martin Davis: An overview of his work in logic, computer science, and philosophy. ~ Liesbeth De Mol, Yuri V. Matiyasevich, Eugenio G. Omodeo, Alberto Policriti, Wilfried Sieg, Elaine J. Weyuker. #Logic #Math #CompSci
• Freshman’s dream. ~ John D. Cook. #Math #Python #Programming
• The reasons AI may act secretive (Trained to reflect human behavior, AI models may share half-truths or purposely omit information). ~ Jennifer Goforth Gregory. #AI
• In search of better search (Does AI improve, or misdirect, search engines and their results?). ~ Samuel Greengard. #GenAI
• #Exercitium: Suma de todos los anteriores. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 28 October 2025 are:

• Formalization of Walsh-Fourier series. ~ Izabela Maria Mandla. #ITP #LeanProver #Math
• Towards a verified compiler for Distributed PlusCal. ~ Ghilain Bergeron, Horatiu Cirstea, Stephan Merz. #ITP #LeanProver
• A deterministic descent framework for the Collatz conjecture. ~ Ünver Çiftçi. #ITP #LeanProver #Math
• How important are formal methods and formal logic for software engineering education? ~ Antti Valmari, Veikko Halttunen. #FormalMethods #Logic
• The art and discipline of prompt engineering. ~ Shilpa Shastri. #AI
• #Exercitium: Máximo de una función. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 27 October 2025 are:

• Stock market shark: More multidimensional DP. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. ~ Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh. #ITP #LeanProver #LLM
• #Exercitium: Poner en mayúscula la primera letra y las restantes en minúsculas. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 26 October 2025 are:

• Why formalize mathematics - more than catching errors. ~ Rado Kirov. #ITP #LeanProver #Math
• Path equivalence and automation for integration contours (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• An introduction to formal real analysis (Lecture 13: Monotone subsequence). ~ Alex Kontorovich. #ITP #LeanProver #Math
• An introduction to formal real analysis (Lecture 14: The Bolzano-Weierstrass theorem). ~ Alex Kontorovich. #ITP #LeanProver #Math
• #Exercitium: Parte impar de un número. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 October 2025 are:

• Gauss: towards autoformalization for the working mathematician. ~ Jared Duker Lichtman, Jesse Han. #AI #Math #Autoformalization #LLM #ITP #LeanProver
• Course "Artificial Intelligence": 1. Introduction to AI. ~ Deepak Kumar. #AI #History
• Course "Artificial Intelligence": 2. Introduction to AI. ~ Deepak Kumar. #AI #History
• Course "Artificial Intelligence": 3. Two early examples of AI systems: SHRDLU and SHAKEY. ~ Deepak Kumar. #AI #History
• Course "Artificial Intelligence": 4. Problem solving as search. ~ Deepak Kumar. #AI #History
• Course "Artificial Intelligence": 5. Game playing. ~ Deepak Kumar. #AI
• Course "Artificial Intelligence": 6. Expert systems. ~ Deepak Kumar. #AI
• Course "Artificial Intelligence": 7. Representing knowledge using logic. ~ Deepak Kumar. #AI #Logic #KRR
• Course "Artificial Intelligence": 8. Logic in Prolog. ~ Deepak Kumar. #AI #Logic #KRR
• Course "Artificial Intelligence": 9. Other knowledge representation formalisms: frames, conceptual dependency, semantic networks. ~ Deepak Kumar. #AI #KRR
• Course "Artificial Intelligence": 10. Robots and rationality. Subsumption architectures. Agent-based AI. IBM's Watson. Second AI winter. ~ Deepak Kumar. #AI
• Course "Artificial Intelligence": 11. Subsymbolic AI. McCulloch-Pitts neuron. The Perceptron. Example implementation. ~ Deepak Kumar. #AI

The readings shared in Bluesky on 24 October 2025 are:

• Revisiting a short proof of Cauchy’s polygonal number theorem and formalizing it in Lean 4. ~ Kevin K. H. Cheung, Tomas McNamer. #ITP #LeanProver #Math
• Sphere packing in Lean. ~ Christopher Birkbeck, Sidharth Hariharan, Seewoo Lee, Gareth Ma, Bhavik Mehta, Maryna Viazovska. #ITP #LeanProver #Math

The readings shared in Bluesky on 23 October 2025 are:

• Constructive ordinal exponentiation. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #SetTheory
• Mathematics with large language models as provers and verifiers. ~ Hieu Le Duc, Leo Liberti. #AI #Math #LLM #ITP #LeanProver
• Las mejores películas sobre matemáticas. ~ Eduardo Sastre. #Matemáticas

The readings shared in Bluesky on 22 October 2025 are:

• Formal or not formal? That is the question in AI for theorem proving. ~ Kevin Buzzard. #AI #Math #LLM #ITP #LeanProver
• Formalisation of the Calderón transference principle in ergodic theory. ~ Felix Pernegger. #ITP #LeanProver #Math
• OpenAI researcher forced to delete “embarrassing” tweet claiming huge breakthrough. ~ Frank Landymore. #AI #Math
• Leading OpenAI researcher announced a GPT-5 math breakthrough that never happened. ~ Matthias Bastian. #AI #Math
• PhysLean: A talk for physics undergraduates. ~ Joseph Tooby-Smith. #ITP #LeanProver #Math #Physics
• Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof. ~ Boris Alexeev, ChatGPT, Lean, Dustin G. Mixon. #AI #Math #LLM #ChatGPT #ITP #LeanProver
• Una refutación inusual del problema de Erdős #707: Colaboración humano-IA y el papel de Lean. #AI #Math #LLM #ITP #LeanProver
• #Exercitium: Elementos no repetidos. #Haskell #ProgramaciónFuncional #Matemáticas

Terence Tao ha comentado en Mastodon otro ejemplo interesante de la asistencia informática en matemáticas, que involucra nuevamente a los problemas de Erdös: el Problema #707, anteriormente marcado como "abierto", ahora está "refutado" - con la refutación formalizada en Lean. Pero el camino hacia esa refutación fue bastante inusual, y no encajaba perfectamente en ninguna de las narrativas estándar sobre la IA en las matemáticas.

La refutación inicial fue obra de humanos usando argumentos convencionales, sin ayuda inicial de LLMs. Sin embargo, descubrieron después que el problema ya había sido resuelto tres décadas antes por Hall, un hallazgo que las búsquedas bibliográficas humanas y asistidas por IA no detectaron. Para formalizar su prueba en Lean, los autores, sin experiencia previa, usaron ChatGPT en un proceso de "codificación por vibraciones", logrando generar unas 3000 líneas de código verificadas. Este proceso incluso permitió corregir un error en la formalización original del problema.

Este caso ilustra un uso muy específico y responsable de la IA: no para generar ideas matemáticas, sino para asistir en la creación de código formal verificable. La formalización complementa, pero no reemplaza, la prueba humana central. Debido a su contribución crucial en esta etapa, tanto ChatGPT como Lean aparecen como coautores del artículo, destacando un modelo inusual de colaboración humano-IA.

The readings shared in Bluesky on 21 October 2025 are:

• HITrees: Higher-order interaction trees. ~ Amir Mohammad Fadaei Ayyam, Michael Sammler. #ITP #LeanProver
• Certifying optimal MEV strategies with Lean. ~ Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino. #ITP #LeanProver
• Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Muntac: A verified certificate checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. #ITP #IsabelleHOL
• RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Andrei Kozyrev, Nikita Khramov, Gleb Solovev, Anton Podkopaev. #ITP #Rocq #LLMs
• #Exercitium: Listas equidigitales. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 20 October 2025 are:

• Formalizing Wigner’s semicircle law in Lean. ~ Haoyan Jiang et als. #ITP #LeanProver #Math
• Towards verifying the "Three amigos". ~ Carl Kwan. #ITP #ACL2 #Math
• Pelletier’s problem 24 in Mizar. ~ Alex Nelson. #ITP #Mizar #Logic #Math
• ProofBridge: Auto-formalization of natural language proofs in Lean via joint embeddings. ~ Prithwish Jana et als. #ITP #LeanProver #Autoformalization #LLMs #Math
• Spatial DP: Finding the largest square. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Divisibles por el primero. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 October 2025 are:

• An introduction to formal real analysis (Lecture 12: Cauchy sequences II). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Pushdown automata (in Isabelle/HOL). ~ Kaan Taskin, Tobias Nipkow. #ITP #IsabelleHOL
• An effective method for solving a class of transcendental diophantine equations. ~ Zeyu Cai. #ITP #LeanProver #Math
• Functional reasoning for distributed systems with failures. ~ Haobin Ni, Robbert van Renesse, Greg Morrisett. #ITP #Rocq
• Ax-Prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics. ~ Marco Del Tredici et als. #AI #Math #LLMs #ITP #LeanProver
• GAR: Generative adversarial reinforcement learning for formal theorem proving. Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang. #AI #Math #LLMs #ITP #LeanProver
• Mathematics with large language models as provers and verifiers. ~ Hieu Le Duc, Leo Liberti. #AI #Math #LLMs #ITP #LeanProver

The readings shared in Bluesky on 17 October 2025 are:

• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Yalep: An environment for learning proof in high-school. ~ Frédéric Tran-Minh, Laure Gonnord, Julien Narboux. #ITP #LeanProver #Logic #Math #Teaching
• Yalep (Yet Another Learning Environment for Proof) is a micro language based on Lean for teaching mathematical high-school proofs. ~ Frédéric Tran Minh. #ITP #LeanProver #Logic #Math #Teaching
• Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord, Julien Narboux. #ITP #Logic #Math #Teaching
• Lean4Less: Eliminating definitional equalities from Lean via an extensional-to-intensional translation. ~ Rishikesh Vaishna. #ITP #LeanProver
• Proof strategy extraction from LLMs for enhancing symbolic provers. ~ Jian Fang, Yican Sun, Yingfei Xiong. #ITP #Rocq #LLM
• Z mathematical toolkit in Isabelle/HOL. ~ Simon Foster, Pedro Ribeiro, Frank Zeyda, Jim Woodcock. #ITP #IsabelleHOL
• MASA: LLM-driven multi-agent systems for autoformalization. ~ Lan Zhang, Marco Valentino, André Freitas. #Autoformalization #LLM #ITP #LeanProver #Math
• Great expectations: Unifying statistical theory and programming. ~ Bradley Saul. #ITP #Agda #FunctionalProgramming #Math
• Where is mathematics going? Large language models and Lean proof assistant. ~ John Elliot V. #Math #LLMs #ITP #LeanProver
• Bridging category theory and functional programming for enhanced learning. ~ Fethi Kadhi. #Haskell #FunctionalProgramming #CategoryTheory
• Exploring Arrows for sequencing effects. ~ Chris Penner. #Haskell #FunctionalProgramming
• Non-obvious Haskell idiom: Bind to lambda case. ~ kqr. #Haskell #FunctionalProgramming
• #Exercitium: Actualización de ejercicios del curso 2014-15. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 16 October 2025 are:

• Most proofs are trivial. ~ Lawrence Paulson. #Math #ITP #IsabelleHOL
• An introduction to formal real analysis (Lecture 11: The real numbers I). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Automated Lean proofs for every type. ~ Elizaveta Pertseva. #ITP #LeanProver
• Mathematics with large language models as provers and verifiers. ~ Hieu Le Duc, Leo Liberti. #AI #Math #LLMs #ITP #LeanProver
• Creating a database of motivated proofs. ~ Timothy Gowers. #AI #Math
• Computing is indeed a discipline in crisis. ~ Moshe Vardi. #CompSci
• Libro «Exercitium: Ejercicios de programación funcional con Haskell (Volumen 1: curso 2013–14)». #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 15 October 2025 are:

• Rely-guarantee verification of queue locks with proof support in Isabelle/HOL. ~ Robert J. Colvin, Scott Heiner, Peter Höfner, Roger C. Su. #ITP #IsabelleHOL
• Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. #ITP #CoqProver
• Mechanizing Olver's error arithmetic. ~ Max Fan, Ariel E. Kellison and Samuel D. Pollard. #ITP #Rocq
• Formal verification of Graham’s scan algorithm. ~ Yingjun Lan, Yuxuan Sun. #ITP #Rocq
• Separation logics for probability, concurrency, and security. ~ Kwing Hei Li. #ITP #Rocq
• McTT: A verified kernel for a proof assistant. ~ Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka. #ITP #Rocq #OCaml #FunctionalProgramming
• Formalizando um teorema de classificação para álgebras de Lie solúveis de baixa dimensão em Lean. ~ Gustavo Infanti, Viviana del Barco, Exequiel Rivas, Paul Schwahn. #ITP #LeanProver #Math
• Verifying the functional correctness of Braun trees with LiquidHaskell. ~ Felipe de León, Alberto Pardo, Marcos Viera. #Haskell #FunctionalProgramming #LiquidHaskell
• How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #Haskell #FunctionalProgramming
• Arrows to arrows, categories to queries. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• DRIFT: Decompose, retrieve, illustrate, then formalize theorems. ~ Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras. #AI #Math #LLMs #ITP #LeanProver
• Books to recommend to maths students. ~ Katie Steckles. #Math

The readings shared in Bluesky on 14 October 2025 are:

• Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL
• A formalization of the generalized quantum Stein's lemma in Lean. ~ Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati. #ITP #LeanProver
• ZF style set theory in Knuckledragger I. ~ Philip Zucker. #Python #Logic #SetTheory
• Making change: Array-based dynamic programming. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha. #Math #SetTheory

The readings shared in Bluesky on 13 October 2025 are:

• PVS formalization of proofs of the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro. #ITP #PVS #Math
• Certified decision procedures for width-independent bitvector predicates. ~ Siddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias Grosser. #ITP #LeanProver
• Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. #ITP #CoqProver #Teaching
• Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. #ITP #CoqProver
• Incremental certified programming. ~ Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter. #ITP #Rocq
• Proof repair across quotient type equivalences. ~ Cosmo Viola, Max Fan, Talia Ringer. #ITP #Rocq
• Don’t call us, we’ll call you (Towards mixed-initiative interactive proof assistants for programming language theory). ~ Jan Liam Verter, Tomas Petricek. #ITP #Teaching
• Synthesizing implication lemmas for interactive theorem proving. ~ Ana Brendel, Aishwarya Sivaraman, Todd Millstein. #ITP #Rocq
• Deriving an Erlang interpreter from a mechanised formal semantics of core Erlang. ~ Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Simon Thompson. #ITP #Agda #FunctionalProgramming #Erlang
• Checking a denotational semantics of Scheme in Agda. ~ Peter D. Mosses. #ITP #Agda
• Mechanised proofs of atom exhaustion in Erlang. ~ Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Gergő Lajos Turán. #ITP #Rocq
• Formalizing the zigzag construction of path spaces of pushouts. ~ Vojtěch Štěpančík. #ITP #Agda
• Unification modulo isomorphisms between dependent types for type-based library search. ~ Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe. #Haskell #FunctionalProgramming
• Representing data structures with invariants in Haskell: The cases of BST and AVL. ~ Nicolas Rodriguez, Alberto Pardo, Marcos Viera. #Haskell #FunctionalProgramming
• A formalization of opaque definitions for a dependent type theory. ~ Nils Anders Danielsson, Eve Geng. #ITP #Agda #FunctionalProgramming
• The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. #ITP #Agda #FunctionalProgramming
• A tale of two lambdas: A haskeller’s journey into OCaml. ~ Richard A. Eisenberg. #Haskell #OCaml #FunctionalProgramming
• A Clash course in solving Sudoku (Functional pearl). ~ Gergő Érdi. #Haskell #FunctionalProgramming
• The calculated typer (Functional pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• Plinth: A plugin-powered language built on Haskell. ~ Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel Chakravarty. #Haskell #FunctionalProgramming
• Rebound: Efficient, expressive, and well-scoped binding. ~ Noé De Santo, Stephanie Weirich. #Haskell #FunctionalProgramming
• Total type classes. ~ Robert Weingart, Nicolas Wu. #Haskell #FunctionalProgramming
• Automatic C bindings generation for Haskell. ~ Travis Cardwell, Sam Derbyshire, Edsko de Vries, Dominik Schrempf. #Haskell #FunctionalProgramming
• Lightweight testing of persistent amortized time complexity in the credit monad. ~ Anton Lorenzen. #Haskell #FunctionalProgramming
• Freer arrows and why you need them in Haskell. ~ Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li. #Haskell #FunctionalProgramming
• Staging automatic differentiation with fusion. ~ Samuel Klumpers, Tom Schrijvers. #Haskell #FunctionalProgramming
• An empirical evaluation of property-based testing in Python. ~ Savitha Ravi, Michael Coblenz. #Python #Programming

The readings shared in Bluesky on 11 October 2025 are:

• An introduction to formal real analysis (Lecture 9: Finite sums and boundedness of convergent sequences). ~ Alex Kontorovich. #ITP #LeanProver #Math
• An introduction to formal real analysis (Lecture 10: Algebraic limit theorem and order properties). ~ Alex Kontorovich. #ITP #LeanProver #Math
• #Exercitium: Laberinto numérico. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 10 October 2025 are:

• Markov kernels in Mathlib's probability library. ~ Rémy Degenne. #ITP #LeanProver #Math
• Relational divisibility (in Isabelle/HOL). ~ Walter Guttmann. #ITP #IsabelleHOL #Math
• ADTs, functions and induction. ~ Andrei Arusoaie. #ITP #LeanProver #FunctionalProgramming
• Principles of programming languages (lecture notes for CS2105O2). ~ Andrei Arusoaie. #ITP #CoqProver
• Principles of programming languages: A little bit of history. ~ Andrei Arusoaie. #Programming
• Formal methods in software engineering. ~ Andrei Arusoaie. #FormalMethods
• Languages. Formal Systems. Inference rules. Proofs. ~ Andrei Arusoaie. #FormalMethods #Logic #Dafny
• Mathematicians’ new best friend? ~ Benjamin Skuse. #AI #Math
• #Exercitium: Sustitución en una expresión aritmética. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 9 October 2025 are:

• State management in Haskell. ~ Ajeet Grewal. #Haskell #FunctionalProgramming
• Haskell is the perfect fit for renewable energy tech. ~ Marc Jakobi. #Haskell #FunctionalProgramming
• Mathematics: The rise of the machines. ~ Yang-Hui He. #AI #Math #LLMs #ITP #LeanProver
• #Exercitium: Clausura de un conjunto respecto de una función. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 October 2025 are:

• Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa. #ITP #LeanProver #Mathlib #Math
• #Exercitium: Cadenas de ceros y unos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 7 October 2025 are:

• 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
• The Mondrian introduction to functional optics. ~ Marco Perone. #Haskell #FunctionalProgramming
• Using an LLM on the Advent of Code. ~ Joe Marshall. #Advent_of_Code #AI_coding #CommonLisp #Gemini #LLM
• #Exercitium: Números con todos sus dígitos primos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 6 October 2025 are:

• An introduction to formal real analysis (Lecture 8: Advanced limit theorems and induction). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. #ITP #CoqProver #Math
• Aristotle: IMO-level automated theorem proving. ~ Tudor Achim et als. #AI #Math #LLMs #ITP #LeanProver
• Waitfree linearization of an arbitrary data object. ~ Wim Hendrik Hesselink.2#page=135 #ITP #PVS
• Correctness, artificial intelligence, and the epistemic value of mathematical proof. ~ James Owen Weatherall, Jesse Wolfson. #Math #AI #ITP
• Dynamic programming primer. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Matriz permutación. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 4 October 2025 are:

• Where is mathematics going? ~ Kevin Buzzard. #Math #ITP #LLM
• Functional data structures and algorithms: A proof assistant approach. ~ Tobias Nipkow (Ed.) #ITP #IsabelleHOL #FunctionalProgramming #Algorithms
• A formal Y86 simulator with CHERI features. ~ Carl Kwan , Yutong Xin, William D. Young. #ITP #ACL2
• IMProofBench: Benchmarking AI on research-level mathematical proof generation. ~ Johannes Schmitt et als. #AI #Math #LLMs

The readings shared in Bluesky on 03 October 2025 are:

• Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. #ITP #LeanProver #Mathlib #Math
• The Mathlib initiative (Building the digital foundation of mathematics). #ITP #LeanProver #Mathlib #Math
• Mathematics in the age of automated proofs: What do we tell our students about AI? ~ Akshay Venkatesh. #Math #AI
• Mathematics in the age of automated proofs: AlphaProof (From the lab into your hands). ~ Thomas Hubert. #AI #Math #ITP #LeanProver #AlphaProof
• Mathematics in the age of automated proofs: After Math (historical perspectives on automated intelligence). ~ Stephanie Dick. #AI #Math #ATP
• #Exercitium: Inserción en árboles binarios de búsqueda. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 02 October 2025 are:

• Digitalizing physics into Lean 4. ~ Joseph Tooby-Smith. #ITP #LeanProver #Physics #Math
• A very early history of algebraic data types. ~ Hillel Wayne. #FunctionalProgramming
• The Haskell Unfolder Episode 48: Safe coercions. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 01 October 2025 are:

• A PVS library on the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro, Mariano M. Moscato, Thaynara Arielly de Lima, Mauricio Ayala-Rincón. #ITP #PVS #Math
• An introduction to formal real analysis (Lecture 7: Uniqueness and advanced limit theorems). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Agentic Lean Auformalization (ALA): An LLM collaborative approach to autoformalization in LEAN. ~ Patricio Gallardo, Maziar Raissi, Ke Zhang, Sudhir Murthy. #Autoformalization #ITP #LeanProver #LLMs
• Hilbert: Recursively building formal proofs with informal reasoning. ~ Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, Ke Ye. #AI #Math #LLMs #ITP #LeanProver
• Formalizing Mason-Stothers theorem and its corollaries in Lean 4. ~ Jineon Baek, Seewoo Lee. #ITP #LeanProver #Math
• Nominal sets in Rocq. ~ Fabrício Sanches Paranhos, Daniel Ventura. #ITP #Rocq #Math
• Category theory illustrated: Natural transformations. ~ Jencel Panic. #CategoryTheory

The readings shared in Bluesky on 30 September 2025 are:

• Lean 4 formalizes Mason‑Stothers theorem and polynomial corollaries. #ITP #LeanProver #Math
• #Exercitium: Producto de matrices como listas de listas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 September 2025 are:

• A new proof for soundness of right-forward closures for termination analysis. ~ René Thiemann. #ITP #IsabelleHOL
• Core matrix interpretations for proving termination of term rewrite systems. ~ Ulysse Le Huitouze, René Thiemann. #ITP #IsabelleHOL
• Composition direction of Seymour’s theorem for regular matroids — formally verified. ~ Martin Dvorak et als. #ITP #LeanProver
• Determinism types for functional logic programming. ~ Michael Hanus, Kai-Oliver Prott. #ITP #Rocq
• Cetera: Certified termination with Agda. ~ Dieter Hofbauer, Johannes Waldmann. #ITP #Agda
• Apply the trie: Word search. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang

The readings shared in Bluesky on 28 September 2025 are:

• Nondeterministic asynchronous dataflow in Isabelle/HOL. ~ Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel. #ITP #IsabelleHOL
• Formalizing splitting in Isabelle/HOL. ~ Ghilain Bergeron, Florent Krasnopol, Sophie Tourret. #ITP #IsabelleHOL
• L-mosaics and bounded join-semilattices in Isabelle/HOL. ~ Alessandro Linzi. #ITP #IsabelleHOL
• Reaping the first fruits of the Isabelle/RL project. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL
• Formalizing the Dershowitz-Manna ordering theorem in Lean 4. ~ Haitian Wang. #ITP #LeanProver
• An introduction to formal real analysis (Lecture 6: Advanced proof techniques and the squeeze theorem). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot, Thomas Portet. #ITP #Rocq
• Quantifiers for differentiable logics in Rocq. ~ Jairo Miguel Marulanda-Giraldo et als. #ITP #Rocq
• Theorem provers and the future AI math ecosystem. ~ Stephan Schulz. #AI #Math #LLMs #ATP
• Monads are too powerful: The expressiveness spectrum. ~ Chris Penner. #Haskell #FunctionalProgramming
• #Exercitium: Sucesiones pucelanas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 26 September 2025 are:

• Composition direction of Seymour's theorem for regular matroids formally verified. ~ Martin Dvorak et als. #ITP #LeanProver #Math
• Generous donation to advance AI for mathematics. ~ Christiana Jasutan. #AI #Math #ITP #LeanProver

The readings shared in Bluesky on 25 September 2025 are:

• Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. #ITP #LeanProver #Math
• Micrograd in Haskell: Evaluation and backward pass. ~ Ajeet Grewal #Haskell #FunctionalProgramming
• Gödel test: Can large language models solve easy conjectures? ~ Moran Feldman, Amin Karbasi. #LLMs #Math

The readings shared in Bluesky on 24 September 2025 are:

• List of crowdsourced math projects actively seeking participants. ~ Terence Tao et als. #Math
• PenroseKiteDart user guide. ~ Chris Reade. #Haskell #FunctionalProgramming
• #Exercitium: Todas tienen par. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 23 September 2025 are:

• Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• A formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz et als. #ITP #IsabelleHOL #Math
• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Formalizing splitting in Isabelle/HOL. ~ Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. #ITP #IsabelleHOL
• Formalizing the hidden number problem in Isabelle/HOL. ~ Sage Binder, Eric Ren, and Katherine Kosaian. #ITP #IsabelleHOL #Math
• Abstract, compositional consistency: Isabelle/HOL locales for completeness à la Fitting. ~ Asta Halkjær From, Anders Schlichtkrull. #ITP #IsabelleHOL #Logic
• An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems. ~ Dohan Kim. #ITP #IsabelleHOL
• Animating MRBNFs: Truly modular binding-aware datatypes in Isabelle/HOL. ~ Jan van Brügge, Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL
• Improving the SMT proof reconstruction pipeline in Isabelle/HOL. ~ Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. #ITP #IsabelleHOL
• Nondeterministic asynchronous dataflow in Isabelle/HOL. ~ Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. #ITP #IsabelleHOL
• Verifying an efficient algorithm for computing Bernoulli numbers. ~ Manuel Eberl and Peter Lammich. #ITP #IsabelleHOL #Math
• Verification of the CVM algorithm with a functional probabilistic invariant. ~ Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, and Yong Kiam Tan. #ITP #IsabelleHOL
• A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• Finiteness of symbolic derivatives in Lean. ~ Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner. #ITP #LeanProver #Math
• Formalizing colimits in Cat. ~ Mario Carneiro and Emily Riehl. #ITP #LeanProver #CategoryTheory
• Canonical for automated theorem proving in Lean. ~ Chase Norman and Jeremy Avigad. #ITP #LeanProver
• Algebra is half the battle: Verifying presentations of graded unipotent Chevalley groups. ~ Eric Wang et als. #ITP #LeanProver #Math
• Automatically generalizing proofs and statements. ~ Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers. #ITP #LeanProver
• Verifying datalog reasoning with Lean. ~ Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. #ITP #LeanProver
• LeanLTL: A unifying framework for linear temporal logics in lean. ~ Eric Vin, Kyle A. Miller, and Daniel J. Fremont. #ITP #LeanProver
• Certified implementability of global multiparty protocols. ~ Elaine Li and Thomas Wies. #ITP #Rocq
• Formalizing concentration inequalities in Rocq: Infrastructure and automation. ~ Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. #ITP #Rocq
• Formally verifying a vertical cell decomposition algorithm. ~ Yves Bertot and Thomas Portet. #ITP #Rocq
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs. #ITP #Rocq
• Towards automating permutation proofs in Rocq: A reflexive approach with iterative deepening search. ~ Nadeem Abdul Hamid. #ITP #Rocq
• Formalising subject reduction and progress for multiparty session processes. ~ Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida. #ITP #CoqProver
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. #ITP #Agda
• A verified cost model for call-by-push-value. ~ Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. #ITP #HOL4
• GOL in GOL in HOL: Verified circuits in Conway’s game of life. ~ Magnus O. Myreen and Mario Carneiro. #ITP #HOL4
• Mechanising Böhm trees and λη-completeness. ~ Chun Tian and Michael Norrish. #ITP #HOL4
• Barendregt’s theory of the λ-calculus, refreshed and formalized. ~ Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. #ITP #Abella
• A natural language formalization of perfectoid rings in ℕaproche. ~ Peter Koepke. #ITP #Naproche #Math
• Adhesive category theory for graph rewriting in Rocq. ~ Samuel Arsac, Russ Harmer, Damien Pous. #ITP #Rocq
• Writing our own structure: Tries in Haskell & Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang

The readings shared in Bluesky on 22 September 2025 are:

• Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin et als. #ITP #LeanProver
• Computationally-sound symbolic cryptography in Lean. ~ Stefan Dziembowski et als. #ITP #LeanProver
• Formal verification of the Euler Sieve via Lean. ~ Isaac (Rucheng) Li. #ITP #LeanProver #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers (video). ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver #ATP #SMT
• Determination of the fifth Busy Beaver value. ~ Justin Blanchard et als. #ITP #CoqProver #Rocq
• Discovering new theorems via LLMs with in-context proof learning in Lean. ~ Kazumi Kasaura et als. #ITP #LeanProver #Math #LLMs
• Refinement-types driven development: A study. ~ Facundo Domínguez, Arnaud Spiwack. #FunctionalProgramming #Liquid #Haskell #SMT
• Feeling cranky about AI and CS education. ~ Valerie Barr. #AI #CompSci #Education
• AWS scientist: Your AI strategy needs mathematical logic. ~ Byron Cook. #AI #LLMs #Logic #Math #ATP #ITP
• #Exercitium: Producto cartesiano de una familia de conjuntos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 20 September 2025 are:

• Everything you know is wrong. ~ Lawrence Paulson. #AI #Logic #ATP #ITP #FunctionalProgramming #LogicProgramming #FormalVerification
• An introduction to formal real analysis (Lecture 4: Non-convergence of (-1)ⁿ, triangle inequality). ~ Alex Kontorovich. #ITP #LeanProver #Math
• An introduction to formal real analysis (Lecture 5: Doubling a convergent sequence). ~ Alex Kontorovich. #ITP #LeanProver #Math

The readings shared in Bluesky on 19 September 2025 are:

• Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. #ITP #LeanProver
• The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction. ~ Arnaud Mayeux, Jujian Zhang. #ITP #LeanProver
• The groupoid-syntax of type theory is a set. ~ Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie. #ITP #Agda
• Mechanizing the meta-theory of session types in Rocq: A tutorial. ~ Marco Carbone, Alberto Momigliano. #ITP #Rocq
• Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. #ITP #CoqProver #Idris2
• The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. #ITP #Agda

The readings shared in Bluesky on 18 September 2025 are:

• Case study: Verified Vampire proofs in the lambdapi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suda. #ATP #Vampire #ITP #Dedukti
• Gemini AI solves coding problem that stumped 139 human teams at ICPC World Finals (Gemini shows off at another high-level academic competition). ~ Ryan Whitwam. #AI #LLMs #Gemini #Programming
• #Exercitium: Código Morse. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 17 September 2025 are:

• Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin, Colin Jones, John Velkey, Tyler R. Josephson. #ITP #LeanProver
• Claude can (sometimes) prove it. ~ Mike Dodds. #ITP #LeanProver #Math #AI #LLMs #Claude
• Structuring definitions in mathematical libraries. ~ Alena Gusakov, Peter Nelson, Stephen Watt. #ITP #LeanProver #Math
• A blueprint for the formalization of Carleson’s theorem on convergence of Fourier series. ~ Lars Becker et als. #ITP #LeanProver #Math
• Formalization of the internal language of a topos. ~ Johannes Folttmann. #ITP #LeanProver #Math
• The meta-principle: A tautological foundation for physics. ~ Jonathan Washburn. #ITP #LeanProver #Physics
• Łukasiewicz logic with actions for neural networks training. ~ Ioana Leuştean, Bogdan Macovei. #ITP #LeanProver
• Towards automated mathematical discovery. ~ Aaron Courville, Navin Goyal. #AI #Math #LLMs #ITP #LeanProver
• Sketchpad: A high-precision and easy-to-use system for automatic formal sketch generation. ~ Wenda Li, Luo Mai, Larry Paulson, Huajian Xin. #AI #Math #ITP #IsabelleHOL #LeanProver
• Scalable theorem proving via mathematical databases. ~ Christopher Birkbeck, David Roe, Andrew Sutherland. #AI #Math #ITP #LeanProver
• Learning to do math with vampires and spiders. ~ Andrei Voronkov, Michael Rawson. #ITP #LeanProver #Rocq
• GNN-SMT: A consortium based proof automation for Lean 4. ~ Clark Barrett, Leni Aniva, Abdalrhman Mohamed, Harun Khan. #ITP #LeanProver #SMT
• Game over or QED? (For taking the Lean Game Server to the next level). ~ Marcus Zibrowius. #ITP #LeanProver
• Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. #ITP #LeanProver #Mathlib
• Document-level autoformalization. ~ Antoine Bosselut, Viktor Kunčak, Maryna Viazovska. #AI #Math #ITP #LeanProver #Autoformalization
• Databases of structured motivated proofs. ~ Timothy Gowers, Anand Rao, Anshula Gandhi, Jacob Loader, Jovan Gerbscheid, Jonas Bayer. #AI #Math #ITP #LeanProver
• Constraining LLMs for theorem proving (A neurosymbolic approach to guaranteed autoformalization). ~ Eleonora Giunchiglia, Sam Adam-Day, Joshua Ong, Mihaela Cătălina Stoian, Luca Andolfi. #AI #Math #LLMs #ITP #LeanProver #Autoformalization
• Bridging proof and computation (For a verified Lean–Macaulay2 interface). ~ Matthew Ballard, Anton Leykin, Damiano Testa, Michael Stillman. #AI #Math #ITP #LeanProver #CAS #Macaulay2
• A structured representation of tactics for machine-assisted theorem proving. ~ Jade Master, Vincent Wang-Maścianica, Zanzi Mihejevs, Bruno Gavranović, Andre Videla, Dylan Braithwaite. #AI #Math #ITP #LeanProver
• A dataset of modern formalized theorem statements. ~ Kevin Buzzard. #ITP #LeanProver #Math
• An AI-focused tactic for language learning. ~ Robert Y. Lewis. #AI #Math #ITP #LeanProver
• Quantum structures and functional programming. ~ Jerzy Karczmarczuk. #Haskell #FunctionalProgramming
• Plinth: A plugin-powered language built on Haskell (Experience report). ~ Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel Chakravarty. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 15 September 2025 are:

• Topological sort: Managing mutable structures in Haskell. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Elemento más cercano que cumple una propiedad. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 14 September 2025 are:

• An introduction to formal real analysis (Lecture 3: More fun with sequences). ~ Alex Kontorovich. #ITP #LeanProver #Math

The readings shared in Bluesky on 13 September 2025 are:

• Greibach normal form (in Isabelle/HOL). ~ Alexander Haberl, Tobias Nipkow, Akihisa Yamada. #ITP #IsabelleHOL
• Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. #ITP #IsabelleHOL

The readings shared in Bluesky on 12 September 2025 are

• Finiteness of symbolic derivatives in Lean. ~ Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner. #ITP #LeanProver #Math
• Modeling and proving in computational type theory using the Rocq prover. ~ Gert Smolka. #ITP #Rocq
• MPCTT textbook project (Modeling and proving in computational type theory using the Rocq prover). ~ Gert Smolka. #ITP #Rocq
• Introducing Gauss, an agent for autoformalization. #AI #Autoformalization #ITP #LeanProver #Math

The readings shared in Bluesky on 11 September 2025 are

• An introduction to Lean 4 (An introduction to formal verification). ~ Enric Cosme Llópez, Lü Gong. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 0: Introduction). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 1: Defining sets and membership). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 2: Subsets). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 3: Properties of subsets). ~ Filip Łajszczak. #ITP #LeanProver #Math
• A Lean 4 formalization of Pólya enumeration theorem. ~ Luka Opravš. #ITP #LeanProver #Math
• Haskell equations, thirty-eight years later. ~ Philip Wadler. #Haskell #FunctionalProgramming
• Better Haskell stack traces via user annotations. ~ Hannes Siebenhandl, Matthew Pickering. #Haskell #FunctionalProgramming
• Fraudulent publishing in the mathematical sciences. ~ Ilka Agricola, Lynn Heller, Wil Schilders, Moritz Schubotz, Peter Taylor, Luis Vega. #Math
• #Exercitium: Representación de Zeckendorf. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 10 September 2025 are

• An introduction to formal real analysis (Lecture 1: The story of real analysis. Lean tactics (exact, rfl, rewrite, ring_nf, use, intro, specialize, choose)). ~ Alex Kontorovich. #ITP #LeanProver #Math
• An introduction to formal real analysis (Lecture 2: Newton's computation of π. Formal definition of the limit of a sequence). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Real analysis, the game! ~ Alex Kontorovich. #ITP #LeanProver #Math
• Using Haskell in production. ~ Agentultra. #Haskell #FunctionalProgramming
• #Exercitium: Ventana deslizante. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 9 September 2025 are

• Higher order differential calculus in Mathlib. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
• Ordinal exponentiation in homotopy type theory. ~ Tom de Jong et als. #ITP #Agda #HoTT #Math
• The story of mathematics. #Math
• La historia de las matemáticas: 35.000 años de números, año arriba, año abajo. ~ @Alvy. #Matemáticas
• #Exercitium: Renombramiento de un árbol. #Haskell #ProgramaciónFuncional
• #Exercitium: Divide si todos son múltiplos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 September 2025 are

• Graph algorithms in board games! ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Empiezan con mayúscula. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 7 September 2025 are

Índice

• Course: Introduction to real analysis. ~ Alex Kontorovich. #Math #ITP #LeanProver
• Introduction to formal real analysis (Lecture 1). ~ Alex Kontorovich. #Math #ITP #LeanProver
• Introduction to formal real analysis (Lecture 2). ~ Alex Kontorovich. #Math #ITP #LeanProver
• #Exercitium: Límite de sucesiones. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 6 September 2025 are

• An introduction to Lean 4. ~ E. Cosme Llópez, L. Gong. #ITP #LeanProver #FunctionalProgramming
• The gap between commercial and open-source LLMs for Olympiad-level math is shrinking. #AI #LLMs #Math

The readings shared in Bluesky on 5 September 2025 are

• Program verification is not all-or-nothing. ~ Lawrence Paulson. #FormalVerification
• The future of math is programming. ~ Ank Yog. #ITP #LeanProver #Math
• AI-driven formal theorem proving. #ITP #LeanProver #AI #LLMs
• Better Haskell stack traces via user annotations. ~ Hannes Siebenhandl, Matthew Pickering. #Haskell #FunctionalProgramming
• What is the Fourier transform?. ~ Shalma Wegsman. #Math
• #Exercitium: Intercalación de n copias. #Haskell #ProgramaciónFuncional
• #Exercitium: Eliminación de n elementos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 4 September 2025 are

• F91 in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Lean: First steps. ~ Tariq Rashid. #ITP #LeanProver
• Acorn and the future of (AI?) theorem proving. ~ Guillermo Angeris. #ITP #LeanProver
• Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. #ITP #IsabelleHOL #LLMs
• Distributors (Unifying parsers, printers & grammars). ~ Eitan Chatav. #Haskell #FunctionalProgramming
• La red social de org-mode. ~ Notxor. #Emacs #OrgMode
• #Exercitium: N gramas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Sopa de letras. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 3 September 2025 are

• Thinking programs (Logical modeling and reasoning about languages, data, computations, and executions). ~ Wolfgang Schreiner. #ITP #IsabelleHOL #Logic #CompSci
• A blueprint for the formalization of Carleson's theorem on convergence of Fourier series. ~ Lars Becker et als. #ITP #LeanProver #Math
• Lean for JavaScript developers. ~ Dan Abramov. #ITP #LeanProver
• Contradiction, contraposition and Lean. ~ Oussama. #ITP #LeanProver
• The meta-principle: A type-theoretic theorem and its interpretation. ~ Jonathan Washburn. #ITP #LeanProver
• Introduction to formal methods using interactive proof assistant Rocq. ~ Evgeny Makarov. #ITP #Rocq
• #Exercitium: Entero positivo de la cadena. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 2 September 2025 are

• Aspects of category theory in proof assistants. ~ Luc Chabassier. #ITP #CoqProver #CategoryTheory
• No-free-lunch theorem for machine learning. ~ Michikazu Hirata. #ITP #IsabelleHOL
• #Exercitium: Actualizaciones de ejercicios. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 1 September 2025 are

• Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. #ITP #LeanProver #Mathlib
• Starting out with graph algorithms: Basic DFS. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• Alpha-beta pruning is just minimax in a lattice of clamping functions. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• #Exercitium: Buscaminas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Mayor sucesión del problema 3n+1. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Filtro booleano. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 31 August 2025 are

• #Exercitium: Descomposiciones como sumas de n sumandos. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Selección hasta el primero que falla inclusive. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 30 August 2025 are

• Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. #ITP #IsabelleHOL
• Demostración incorrecta de P ≠ NP publicada en la revista "Frontiers of Computer Science". ~ Francisco R. Villatoro. #Math
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Número de inversiones. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Eliminación de las ocurrencias aisladas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ordenada cíclicamente. #Haskell #ProgramaciónFuncional
• #Exercitium: Órbita prima. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Divisores de un número con final dado. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 August 2025 are

• Tic-tac-toe meets Lean 4. ~ Adolfo Ochagavía. #ITP #LeanProver
• Continuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda
• Erdös problems. ~ Thomas Bloom. #Math
• #Exercitium: Números triangulares con n cifras distintas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Enumeración de árboles binarios. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Elementos de una matriz con algún vecino menor. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Reiteración de una función. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Pim, Pam, Pum y divisibilidad. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Código de las alergias. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Índices de valores verdaderos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 28 August 2025 are

• Haskell Course: Lesson 21: Reader, Writer, and State Monads. ~ Robertino Martinez. #Haskell #FunctionalProgramming
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Elemento más repetido de manera consecutiva. #Haskell #ProgramaciónFuncional
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Mayor producto de las ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Biparticiones de una lista. #Haskell #ProgramaciónFuncional
• #Exercitium: Trenzado de listas. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 27 August 2025 are

• Basic category theory. ~ Tom Leinster. #eBook #CategoryTheory
• #Exercitium: Segmentos maximales con elementos consecutivos. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 26 August 2025 are

• Experimental results for Vampire on the equational theories project. ~ Mikoláš Janota. #ATP #Vampire
• Lean meets theoretical computer science: Scalable synthesis of theorem proving challenges in formal-informal pairs. ~ Terry Jingchen Zhang et als. #ITP #LeanProver #LLMs
• Why cannot large language models ever make true correct reasoning? ~ Jingde Cheng. #LLMs #Reasoning
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Máximos locales. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Lista cuadrada. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 August 2025 are

• Visualizing regular expression NFAs in Lean. ~ Krishna Padmasola. #ITP #LeanProver
• A case study on the effectiveness of LLMs in verification with proof assistants. ~ Barış Bayazıt, Yao Li, Xujie Si. #ITP #Rocq #LLMs
• Big-stop semantics: A simple way to get the benefits of small-step semantics in a big-step judgment. ~ David M Kahn, Jan Hoffmann, Runming Li. #ITP #Agda
• Formalizing axiomatic theories of truth. ~ Bram Swaanen. #ITP #LeanProver #Logic
• Introduction to proofs using Waterproof. ~ Alex van Tilburg. #ITP #Rocq #Waterproof
• Sets & heaps in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Primos equidistantes. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 24 August 2025 are

• LeanGeo: Formalizing competitional geometry problems in Lean. ~ Chendong Song et als. #ITP #LeanProver #Math #LLMs
• To zip through the cost analysis of probabilistic programs. ~ Matthias Hetzenberger, Georg Moser, Florian Zuleger. #Haskell #FunctionalProgramming
• #Exercitium: Mastermind. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Anagramas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 23 August 2025 are

• Formalizing class field theory. ~ Georgia Harbor-Collins, Mohit Hulse. #ITP #LeanProver #Math
• Decidable equality for indexed data types, take 2. ~ Brent Yorgey. #Agda #FunctionalProgramming #ITP

The readings shared in Bluesky on 22 August 2025 are

• Definite integrals, II: improper integrals. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Continuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. #ITP #Agda #Math
• Reasoning about weak isolation levels in separation logic. ~ Anders Alnor Mathiasen et als. #ITP #Rocq
• The Baby paradox in Haskell. ~ Justin Le. #Haskell #FunctionalProgramming #Logic
• Applicative-wired monad pattern. ~ Chris Done. #Haskell #FunctionalProgramming
• #Exercitium: Iguales al siguiente. #Haskell #FunctionalProgramming
• #Exercitium: Ordenación por el máximo. #Haskell #FunctionalProgramming
• #Exercitium: La bandera tricolor. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Determinación de los elementos minimales. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 20 August 2025 are

• Queen domination by SAT solving. ~ Taha Rostami, Curtis Bright. #ATP #SAT_Solving
• The price of intelligence (Three risks inherent in LLMs). ~ Mark Russinovich, Ahmed Salem, Santiago Zanella-Béguelin, Yonatan Zunger. #AI #LLMs
• #Exercitium: Problemas de programación con Haskell (noviembre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (octubre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (julio de 2014). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2014). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 19 August 2025 are

• Granite: A library for producing terminal plots. It depends only on Haskell's base package so it should be easy to use and install. ~ Michael Chavinda. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell (diciembre de 2014). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 August 2025 are

• Formalizing axiomatics for first-order logic. ~ Jørgen Villadsen, Simon Tobias Lund, Anders Schlichtkrull. #ITP #IsabelleHOL #Logic
• Formal correctness proofs for efficient CHAD. ~ Benjamin Meijs. #ITP #Agda
• Binary tree BFS: Zigzag order. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Problemas de programación con Haskell (marzo de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (enero de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 17 August 2025 are

• Beyond booleans. ~ Dan Abramov. #ITP #LeanProver
• Counterpart-based quantified temporal logics. ~ Fabio Gadducci, Andrea Laretto, Davide Trotta. #ITP #Agda
• Type soundness of functional languages with subtyping in Lang-n-Prove. ~ Matteo Cimini, Joan Montas. #ITP #Abella
• Invertible syntax without the tuples (Functional Pearl). ~ Mathieu Boespflug, Arnaud Spiwack. #Haskell #FunctionalProgramming
• Understanding Fermat's Last Theorem's proofs. ~ Alex Qiu et als. #Math

The readings shared in Bluesky on 16 August 2025 are

• #Exercitium: Problemas de programación con Haskell (junio de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 15 August 2025 are

• Definite integrals, I: easy cases over finite intervals. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Revisiting the Fast Fourier Transform in Rocq. ~ Laurent Théry. #ITP #Rocq #Math
• The Vampire diary. ~ Filip Bártek et als. #ATP #Vampire
• HaLLMos: Expert-guided AI for learning to write mathematical proofs. #Math #AI
• HaLLMos (IA para aprender a escribir demostraciones matemáticas). #Math #AI
• #Exercitium: Problemas de programación con Haskell (diciembre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (noviembre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (octubre de 2015). #Haskell #ProgramaciónFuncional #Matemáticas

HaLLMos es un sistema de inteligencia artificial gratuito diseñado para ayudar en la redacción de pruebas matemáticas de nivel básico. El sistema revisa borradores, identifica lagunas en el razonamiento y facilita el proceso de iteración sin revelar directamente la respuesta.

Es completamente gratuito, funciona desde el navegador web y no requiere crear una cuenta. Los usuarios pueden elegir entre ejercicios introductorios para aprender técnicas de demostración o utilizar el espacio de pruebas libre para trabajar con sus propios problemas.

The readings shared in Bluesky on 14 August 2025 are

• Type inference for plain data. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
• Type-machine (Using Template Haskell to derive the structure of records and simulate structural subtyping). ~ Arthur Jamet. #Haskell #FunctionalProgramming
• Using traversals to batch database queries. ~ Chris Penner. #Haskell #FunctionalProgramming
• The grind tactic. #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell (enero de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 13 August 2025 are

• In-order traversal in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• First analysis lecture (June 16, 2025). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Second analysis lecture "Filter" (June 17, 2025). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Structures in Lean4 (June 20, 2025). ~ Filippo Nuccio. #ITP #LeanProver
• Blueprints and PNT (June 23, 2025). ~ Alex Kontorovich. #ITP #LeanProver
• The Infinity Project (How to use AI and mathematics to prove and improve science and security). ~ Patrick Shafto. #AI #Math #ITP #LeanProver
• Verificación formal en ACL2 de polinomios de múltiples variables y su aplicación al problema de la decisión en la lógica proposicional clásica. ~ Francisco Palomo Lozano. #ITP #ACL2 #Logic #Math
• Reseña de «The Infinity Project (How to use AI and mathematics to prove and improve science and security)». #AI #Math #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell (febrero de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

En el artículo «The Infinity Project (How to use AI and mathematics to prove and improve science and security)» se propone invertir 112,5 MUSD en un concurso entre institutos de matemáticas para formalizar el conocimiento matemático en programas verificables. Con IA y lenguajes como Lean, se busca traducir y validar pruebas, democratizando el acceso a las matemáticas.

El objetivo es aplicar esta infraestructura para aumentar el rigor científico y reforzar la ciberseguridad. Formalizar teorías y procesos permitiría optimizar la investigación, prevenir fallos en sistemas críticos y reducir vulnerabilidades, con beneficios económicos y sociales significativos.

El plan incluye crear una amplia biblioteca matemática, entrenar IA para generar nuevo conocimiento útil y mostrar aplicaciones prácticas. Se plantea una colaboración entre academia, industria y gobiernos, con el potencial de abrir nuevas industrias y transformar ciencia, tecnología y seguridad.

The readings shared in Bluesky on 9 August 2025 are

• Mission-time Linear Temporal Logic Formula Progression (in Isabelle/HOL). ~ Katherine Kosaian, Zili Wang. #ITP #IsabelleHOL
• Two-way deterministic finite automata (in Isabelle/HOL). ~ Felipe Escallón, Tobias Nipkow. #ITP #IsabelleHOL
• Truly functional solutions to the longest uptrend problem (Functional pearl). ~ Alexander Dinges, Ralf Hinze. #Haskell #FunctionalProgramming
• Teaching introductory functional programming using Haskelite. ~ Pedro Vasconcelos. #Haskell #FunctionalProgramming
• Macros in Prolog: Term and goal expansion. ~ Markus Triska. #Prolog #LogicProgramming
• Mathematicians question AI performance at International Math Olympiad. ~ Emily Riehl. #AI #Math #IMO
• Geoint-R1: Formalizing multimodal geometric reasoning with dynamic auxiliary constructions. ~ Jingxuan Wei et als. #ITP #LeanProver #LLMs
• #Exercitium: Problemas de programación con Haskell (diciembre de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 10 August 2025 are

• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa, #ITP #CoqProver
• Domain-specific tensor languages. ~ Jean-Philippe Bernardy, Patrik Jansson. #Haskell #FunctionalProgramming
• Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. #ITP #Agda #FunctionalProgramming
• GradSTL: Comprehensive signal temporal logic for neurosymbolic reasoning and learning. ~ Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL
• A contextual formalization of structural coinduction. ~ Paul Downen, Zena M. Ariol. #FunctionalProgramming
• OCaml Blockly. ~ Kenichi Asai. #OCaml #FunctionalProgramming
• The graphical theory of monads. ~ Ralf Hinze, Dan Marsden. #CategoryTheory
• #Exercitium: Problemas de programación con Haskell (noviembre de 2016). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 August 2025 are

• Discrete mathematics with Lean 4. ~ Shrey Vivek./#/g/shreyvivek/gamemaker #ITP #LeanProver #Math
• Gödel's incompleteness theorem. ~ Thorsten Altenkirch. #ITP #LeanProver #Logic #Math
• Scrutinizing LLM reasoning models (Researchers are seeking to learn the steps behind an LLM's inference process). ~ Emma Stamm. #LLMs #Reasoning
• Cálculo infinitesimal. ~ Gerard Romo Garrido. #eBook #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (enero de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 7 August 2025 are

• Thinking machines: Mathematical reasoning in the age of LLMs. ~ Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen. #AI #LLMs #Math #ITP #LeanProver
• Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. ~ Yong Lin et als. #LLMs #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 6 August 2025 are

• A comparative study of neurosymbolic AI approaches to interpretable logical reasoning. ~ Michael K. Chen. #Neurosymbolic #AI
• #Exercitium: Problemas de programación con Haskell (noviembre de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 5 August 2025 are

• Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir Alex Kontorovich, Heather MacBeth. #ITP #LeanProver #Math
• First analysis lecture (June 16, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• Doing elementary number theory in Lean. ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 1). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 2). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• First geometry lecture (June 17, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second geometry lecture (June 18, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second analysis lecture "Filter" (June 17, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• A crash course on type theory. ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• A crash course on type theory (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• Structures in Lean4 (June 20, 2025). ~ Filippo Nuccio. #ITP #LeanProver
• Blueprints and PNT (June 23, 2025). ~ Alex Kontorovich. #ITP #LeanProver
• Simple groups in Lean. ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Simple groups in Lean (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Metaprogramming in Lean, Talk 1 (June 23, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 2 (June 24, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 3 (June 25, 2025). ~ Heather Macbeth. #ITP #LeanProver
• The Lean FRO year 3 roadmap. #ITP #LeanProver

The readings shared in Bluesky on 4 August 2025 are

• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #CoqProver #AI #LLMs
• Reflections on Haskell@Meta. ~ Simon Marlow. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 3 August 2025 are

• AI at IMO 2025: a round-up. ~ Kevin Buzzard. #AI #LLMs #ITP #LeanProver #Math #IMO
• Formalization of harmonic analysis in Lean. ~ Wouter Bosse. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (diciembre de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 2 August 2025 are

• Solving years-old math problems with Gemini 2.5 Deep Think. ~ Michel van Garrel. #LLMs #Math
• A formalization of multiplicative proof-nets in Rocq. ~ Rémi Di Guardia, Olivier Laurent. #ITP #Rocq
• Fixed-point-oriented programming: A concise and elegant paradigm. ~ Yong Qi Foo, Brian Sze-Kai Cheong, Michael D. Adams. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell (enero de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 1 August 2025 are

• Unconstrained optimization (in Isabelle/HOL). ~ Dustin Bryant. #ITP #IsabelleHOL #Math
• Seed-Prover: Deep and broad reasoning for automated theorem proving. ~ Luoxin Chen et als. #ITP #LeanProver #LLMs #Math
• NuminaMath-LEAN is a large-scale dataset of 100K mathematical competition problems formalized in Lean 4. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (abril de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 31 July 2025 are

• The math is haunted. ~ Dan Abramov. #ProofAssistant #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (julio de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 30 July 2025 are

• Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. #ITP #ProofAssistant #IsabelleHOL #Math
• #Exercitium: Problemas de programación con Haskell (mayo de 2022). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2022). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 July 2025 are

• Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. #FormalVerification #ProofAssistants #CoqProver
• Symbolic world models in Lean 4 for reinforcement learning. ~ Matěj Kripner. #ITP #LeanProver #MachineLearning
• Formal verification of the safegcd implementation. ~ Russell O'Connor, Andrew Poelstra. #FormalVerification #ProofAssistants #CoqProver
• Formal verification of pairing heaps in Rocq. ~ Cosmin-Ionut Visan. #FormalVerification #ProofAssistants #Rocq
• Verified functional graph algorithms using the Rocq prover (Coq). ~ Leopold Frieberger. #FormalVerification #ProofAssistants #Rocq
• Formal verification of leftist and skew heaps in Rocq. ~ Elena Marcela Dumitrache. #FormalVerification #ProofAssistants #Rocq
• Comparing codes: Spiral matrix (another matrix layer problem). ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO
• #Exercitium: Problemas de programación con Haskell (noviembre de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (julio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 28 July 2025 are

• Gödel's first incompleteness theorem (in Lean4). #FormalVerification #ProofAssistant #LeanProver #Logic #Math
• Formalized formal logic (in Lean4). #FormalVerification #ProofAssistant #LeanProver #Logic #Math
• #Exercitium: Problemas de programación con Haskell (enero de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (diciembre de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 27 July 2025 are

• Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming
• McTT: A verified kernel for a proof assistant. ~ Junyoung Jang et als. #ProofAssistants #Rocq
• Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. #ProofAssistant #Agda
• Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. #FormalVerification #ProofAssistant #Agda
• A meta-modal logic for bisimulations (in Isabelle/HOL). ~ Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel. #ITP #IsabelleHOL
• Solving formal math problems by decomposition and iterative reflection. ~ Yichi Zhou et als. #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• Reseña de «Solving formal math problems by decomposition and iterative reflection». #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (febrero de 2019). #Haskell #ProgramaciónFuncional #Matemáticas

El artículo «Solving formal math problems by decomposition and iterative reflection» presenta Delta Prover, un nuevo sistema que resuelve problemas matemáticos complejos. Este agente utiliza un LLM que interactúa con el asistente de pruebas Lean 4. Mediante una descomposición de problemas y una reparación iterativa de las pruebas, el sistema aprende de los errores para construir demostraciones verificables. Alcanza un rendimiento del 95.9% de éxito en los problemas de miniF2F, superando a otros métodos sin necesitar un costoso reentrenamiento del modelo.

The readings shared in Bluesky on 26 July 2025 are

• Higher order logic. ~ Mark Jago. #Logic
• My Emacs writing experience. ~ Sacha Chua. #Emacs #Org
• Finding the shape of my thoughts. ~ Sacha Chua. #Emacs #Org
• Writing experience: My decade with Org. ~ Álvaro Ramírez. #Emacs #OrgMode
• #Exercitium: Problemas de programación con Haskell (junio de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2019). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 July 2025 are

• A formalization of elementary linear algebra: Part I. ~ David Russinoff. #ITP #ACL2 #Math
• A formalization of elementary linear algebra: Part II. ~ David Russinoff. #ITP #ACL2 #Math
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• RV32I in ACL2. ~ Carl Kwan. #ITP #ACL2
• Extended abstract: Partial-encapsulate and its support for floating-point operations in ACL2. ~ Matt Kaufmann, J Strother Moore. #ITP #ACL2
• Lean FRO and Mathlib receive $10M from XTX Markets founder Alex Gerko to further advance the use of AI for mathematical research. #AI4Math #ITP #LeanProver #Math
• A Liquid Haskell kick-start. ~ Xavier Góngora. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de diciembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell de noviembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 24 July 2025 are

• Formally verifying automata for trusted decision procedures. ~ Zhaobo (Aeacus) Sheng. #ITP #LeanProver
• Competitive programming in Haskell: sparse tables. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Four ways of declaring interfaces in Haskell. ~ Marco Perone. #FunctionalProgramming #haskell
• Inlining in the Glasgow Haskell Compiler: empirical investigation and improvement. ~ Celeste Hollenbeck. #Haskell #FunctionalProgramming
• Type-level programming for safer resource management. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 47: Pure parallelism. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• DeepMind and OpenAI achieve IMO Gold. What does it all mean? (What we know, what we would like to know, and what it may take years to know). ~ Ernest Davis, Gary Marcus. #AI #Math #LLMs
• #Exercitium: Problemas de programación con Haskell de enero de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 23 July 2025 are

• Seed-Prover: Reasoning wide and deep for automated math theorem proving. #AI #Math #LLMs #ITP #LeanProver
• Seed-Prover achieves IMO 2025 silver score. #AI #Math #LLMs #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell de febrero de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 22 July 2025 are

• A parametricity-based formalization of semi-simplicial and semi-cubical sets. ~ Hugo Herbelin, Ramkumar Ramachandra. #ITP #Rocq
• Comparing codes: Image rotation (Mutable arrays in Haskell). ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. #LLMs #Math #IMO

The readings shared in Bluesky on 21 July 2025 are

• Representability and formalization of (distributive quasi) relation algebras. ~ Peter Jipsen. #ITP #LeanProver #IsabelleHOL #Rocq #Math
• #Exercitium: Problemas de programación con Haskell de abril de 2020. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell de marzo de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 July 2025 are

• Teaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. #CompSci #Teaching #ITP #LeanProver #ACL2
• CSLib: An open-source Lean 4 library formalizing a significant subsetof undergraduate-level computer science. ~ Clark Barrett et als. #ITP #LeanProver #CompSci
• Quantifiers for differentiable logics in Rocq (Extended abstract). ~ Jairo Miguel Marulanda-Giraldo et als. #ITP #Rocq
• Comparing codes: Binary search in a 2D matrix. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. ~ Xingguang Ji et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 18 July 2025 are

• Formalization of derived categories in Lean/Mathlib. ~ Joël Riou. #ITP #LeanProver #Math
• A formalised approach to the composition of processes over linear resources. ~ Filip Smola. #ITP #IsabelleHOL
• Gödel's incompleteness theorems (in Isabelle/HOL). ~ Lawrence C. Paulson, with Janis Bailitis. #ITP #IsabelleHOL #Logic #Math
• Robust dynamic embedding for gradual typing. ~ Koen Jacobs et als. #ITP #Rocq
• Lean meets theoretical computer science: Scalable synthesis of theorem proving challenges in formal-informal pairs. ~ Terry Jingchen Zhang et als. #LLMs #ITP #LeanProver
• LeanTree: Accelerating white-box proof search with factorized states in Lean 4. ~ Matěj Kripner, Michal Sustr, Milan Straka. #LLMs #ITP #LeanProver
• Prover Agent: An agent-based framework for formal mathematical proofs. ~ Kaito Baba et als. #LLMs #ITP #LeanProver
• Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. #LLMs #ITP #LeanProver #Math
• ProofWala: Multilingual proof data synthesis and theorem-proving. ~ Amitayush Thakur et als. #ITP #LeanProver #CoqProver
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver
• Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. #ITP #LeanProver #Mathlib
• VeriBench: End-to-end formal verification benchmark for AI code generation in Lean 4. ~ Brando Miranda et als. #LLMs #ITP #LeanProver
• The Open Proof Corpus: A large-scale study of LLM-generated mathematical proofs. ~ Jasper Dekoninck et als. #LLMs #Math #Reasoning
• Proof or bluff? Evaluating LLMs on 2025 USA Math Olympiad. ~ Ivo Petrov et als. #LLMs #Math #Reasoning
• RealMath: A continuous benchmark for evaluating language models on research-level mathematics. ~ Jie Zhang et als. #LLMs #Math #Reasoning
• The calculated typer (Functional Pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de junio de 2020. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de mayo de 2020. #Haskell #FunctionalProgramming #Math

The readings shared in Bluesky on 17 July 2025 are

• Teaching mathematics with Lean: Interactive theorem provers in the classroom. ~ Paola Iannone, Gihan Marasingha, Athina Thoma. #ITP #LeanProver #Math
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak, Vladimir Kolmogorov. #ITP #LeanProver #Math
• Scott's representation theorem and the univalent Karoubi envelope. ~ Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens. #ITP #Rocq
• #Exercitium: Problemas de programación con Haskell de enero de 2021. #Haskell #FunctionalProgramming