The readings shared in Bluesky on 9 January 2026 are:

Las lecturas compartidas en Bluesky el 9 de enero de 2026 son

• Mathematical understanding. ~ Jeremy Avigad. #Math #AI

The readings shared in Bluesky on 4 January 2026 are:

• Terry Tao on the future of mathematics. #AI #Math #ITP #LeanProver
• Seemingly impossible programs in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Pursuit of truth and beauty in Lean 4 (Formally verified theory of grammars, optimization, matroids). ~ Martin Dvořák. #ITP #LeanProver
• Computing and formalizing residuated lattices and relation algebras. ~ Peter Jipsen. #ITP #LeanProver
• cLean: A verified domain-specific language for GPU kernel programming in Lean 4. ~ Riyaz Ahuja. #ITP #LeanProver
• Lecture Notes: Computational mathematics and AI (A ten-lecture workshop series). ~ Lars Ruthotto. #AI #Math
• An introduction to proofs and the mathematical vernacular. ~ Martin Day. #Math
• Open textbook initiative (The American Institute of Mathematics (AIM)). #Math
• Open textbook library: Mathematics textbooks. #Math
• Emacs Lisp Elements: EPUB and PDF versions now available. ~ Protesilaos Stavrou. #Emacs #Lisp

The readings shared in Bluesky on 29 December 2025 are:

• Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT
• The biggest controversy in maths could be settled by a computer. Alex Wilkins. #ITP #LeanProver #Math
• Report on the current situation surrounding inter-universal Teichmüller theory (IUT). ~ Shinichi Mochizuki. #Math #ITP #LeanProver
• The machine-checked complete formalization of Landau’s foundations of analysis in Rocq. ~ Yue Guan, Yaoshun Fu, Xiangtao Meng. #ITP #Rocq #Math
• Formal verification of Borrow-Checking by local commutation diagrams. ~ Alban Reynaud Michez. #ITP #Rocq
• The unnegatable loop: Tetralemma's performative geometry (with Coq-verification). ~ Siegfried Meister. #ITP #CoqLang
• Une sémantique de Kahn mécanisée pour les machines à états. ~ Timothy Bourke, Paul Jeanmaire, Marc Pouzet. #ITP #Rocq
• Algebraizing higher-order effects. ~ Martin Andrieux, Alan Schmitt. #ITP #Agda
• NAMOR: a new Agda library for modal extended sequents. ~ Riccardo Borsetto, Margherita Zorzi. #ITP #Agda
• Formalisation de la stabilité de l’erreur d’estimation de l’inclinaison d’un robot. ~ Lynda Bentoucha, Reynald Affeldt. #ITP #Rocq
• Tacq: Context aware tactic recommendation for Rocq. ~ Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias, Marc Lelarge, Theo Stoskopf. #ITP #Rocq
• Assignments and strategies in democratic forking analysed with Isabelle/HOL. ~ Jan-Georg Smaus. #ITP #IsabelleHOL
• Dynamic pushdown networks (in Isabelle/HOL). ~ Peter Lammich. #ITP #IsabelleHOL
• Set reconciliation (in Isabelle/HOL). ~ Paul Hofmeier, Emin Karayel. #ITP #IsabelleHOL
• On the design and implementation of Modular Explicits. ~ Samuel Vivien, Didier Rémy, Gabriel Scherer. #OCaml #FunctionalProgramming
• Mapping and explaining syntax errors with LRgrep. ~ Frédéric Bour, François Pottier. #OCaml #FunctionalProgramming
• Cairn : Trouver son chemin dans Menhir. ~ Vincent Penelle. #OCaml #FunctionalProgramming
• Advent of Code 2025: Haskell solution reflections for all 12 days. ~ Justin Le. #Haskell #FunctionalProgramming
• Carnap: a free and open software framework written in Haskell for teaching and studying formal logic. #Haskell #FunctionalProgramming #Logic
• Vibe reasoning: Eliciting frontier AI mathematical capabilities (A case study on IMO 2025 Problem 6). ~ Jiaao Wu, Xian Zhang, Fan Yang, Yinpeng Dong. #AI #Math
• Advice for amateur mathematicians on writing and publishing papers. ~ Henry Cohn. #Math
• #Exercitium: Listas disjuntas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 24 December 2025 are:

• From zero to QED: An informal introduction to formality with Lean 4. ~ Stephen Diehl. #ITP #LeanProver
• A verified implementation of the Misra and Gries edge coloring algorithm. ~ Arohee Bhoja. #ITP #LeanProver
• Formalising differential geometry in Lean. ~ Michael B. Rothgang. #ITP #LeanProver #Math
• Metaprogramming your IDE in Lean 4. ~ Harry Goldstein, Richard Feldman. #ITP #LeanProver
• Gödel's Poetry. ~ Kelly J. Davis. #ITP #LeanProver #AI #LLMs
• #Exercitium: 2015 y los números pitagóricos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 19 December 2025 are:

• Proof engineering for program logics in Isabelle/HOL. ~ Chelsea L. Edmonds. #ITP #IsabelleHOL
• Modular proofs in Isabelle/HOL. ~ Chelsea L. Edmonds. #ITP #IsabelleHOL
• Prediction: AI will make formal verification go mainstream. ~ Martin Kleppmann. #AI #LLMs #ITP #LeanProver #IsabelleHOL #Rocq
• Mathematics in the age of Large Language Models. ~ Przemyslaw Chojecki. #AI #Math
• Advancing mathematics research with generative AI. ~ Lisa Carbone. #AI #Math #ITP #LeanProver
• El triángulo de Pascal y las ternas pitagóricas. ~ Miguel Ángel Morales. #Matemáticas

The readings shared in Bluesky on 14 December 2025 are:

• A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. #ITP #Rocq
• A modular Lean 4 framework for confluence and strong normalization of lambda calculi with products and sums. ~ Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz, Tiago de Veras. #ITP #LeanProver
• Learning about proof with the theorem prover Lean: the abundant numbers task. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math
• So, computers can prove theorems (in Lean), what’s next? ~ Alex J. Best. #AI #Math #ITP #LeanProver
• Lessons from the PrimeNumberTheorem+ project and real analysis game. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Challenges in (auto)formalizing category theory. ~ Emily Riehl. #ITP #LeanProver #Math
• The making of Lean. ~ Leo de Moura. #ITP #LeanProver
• The Carleson project: formalization and collaboration. ~ Michael B. Rothgang. #ITP #LeanProver
• Differential geometry in Mathlib. ~ Michael B. Rothgang. #ITP #LeanProver
• Brownian motion and stochastic integrals. ~ Rémy Degenne et als. #ITP #LeanProver #Math
• Probability theory in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Math
• The Haskell Unfolder Episode 52: Bidirectional parsing and printing (of JSON). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Desemparejamiento de listas. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 10 December 2025 are:

• Complex bounded operators in Isabelle/HOL. ~ Dominique Unruh, José Manuel Rodríguez Caballero. #ITP #IsabelleHOL #Math
• Formalization of Auslander-Buchsbaum-Serre criterion in Lean4. ~ Naillin Guan, Yongle Hu. #ITP #LeanProver #Math
• A certifying proof assistant for synthetic mathematics in Lean. ~ Wojciech Nawrocki et als. #ITP #LeanProver
• An introduction to formal real analysis (Lecture 25: Swapping limits and integrals). ~ Alex Kontorovich. #ITP #LeanProver #Math
• #Exercitium: Representaciones de matrices. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 9 December 2025 are:

• The equational theories project: Advancing collaborative mathematical research at scale. ~ Terence Tao et als. #ITP #LeanProver #Math
• Formalized Hopfield networks and Boltzmann machines. ~ Matteo Cipollina, Michail Karatarakis, Freek Wiedijk. #ITP #LeanProver
• The story of Erdős problem #1026. ~ Terence Tao. #AI #Math #ITP #LeanProver #Aristotle #AlphaEvolve
• Formalisation of security for federated learning with DP and attacker advantage in IIIf for satellite swarms. ~ Florian Kammüller. #ITP #IsabelleHOL
• Candle: A verified implementation of HOL Light. ~ Oskar Abrahamsson et als. #ITP #HOL4 #HOL_Light
• #Exercitium: Permutación de elementos consecutivos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 8 December 2025 are:

• Formalizing polynomial laws and the universal divided power algebra. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• #Exercitium: Juego de bloques con letras. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 7 December 2025 are:

• 50 years of proof assistants. ~ Lawrence Paulson. #ITP #IsabelleHOL #CoqProver #HOL
• DeepWiki leanprover-community/mathlib4: A comprehensive database of formalized theorems in Lean 4. #ITP #LeanProver #Math
• The Seifert-van Kampen theorem via computational paths: A formalized approach to computing fundamental groups. ~ Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. #ITP #LeanProver #Math
• Teaching Prolog and logic programming with Jupyter Notebooks. ~ Galileo Sartor, Adam Wyner. #Prolog #LogicPO
• Functional Python programming in introductory computer science courses. ~ Rajshekhar Sunderraman. #Python #FunctionalProgramming
• #Exercitium: Números que sumados a su siguiente primo dan primos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 6 December 2025 are:

• An introduction to formal real analysis (Lecture 24: Topology). ~ Alex Kontorovich. #ITP #LeanProver #Math

The readings shared in Bluesky on 5 December 2025 are:

• Formalization of Erdős problems. ~ Boris Alexeev. #ITP #LeanProver #Math #Autoformalization
• A Rocq formalization of monomial and graded orders. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. #ITP #Rocq #Math
• Certified G2 manifold construction. ~ Brieuc de La Fournière. #ITP #LeanProver
• Automated reasoning for uncertain Markov processes. ~ Muhammad Maaz. #ATP #SMT #Z3
• Haskell is a great language for data science. ~ Jonathan Carroll. #Haskell #FunctionalProgramming #DataScience #Rstats
• Reseña de «Formalization of Erdős problems». #ITP #LeanProver #Math #Autoformalization
• #Exercitium: Normalización de expresiones aritméticas. #Haskell #ProgramaciónFuncional #Matemáticas

El artículo «Formalization of Erdős problems» destaca el auge en la resolución de problemas de Paul Erdős gracias a la web erdosproblems.com y el proyecto Formal Conjectures. De más de 1100 problemas recopilados, el 40% ya están resueltos y unos 240 tienen sus enunciados formalizados en Lean. Esta infraestructura comunitaria y el uso de bases de datos han acelerado notablemente el progreso matemático.

La gran revolución descrita es el uso de IA para formalizar y resolver estos retos. Herramientas como Aristotle ya no solo asisten, sino que traducen demostraciones de lenguaje natural a código Lean automáticamente. Incluso han logrado hitos históricos al resolver problemas abiertos (como el problema 124) de forma totalmente autónoma, generando nuevas matemáticas verificadas sin ayuda humana.

Finalmente, el autor advierte sobre la "malformalización": errores sutiles al traducir enunciados a código, desde bugs técnicos hasta la omisión de hipótesis necesarias. A pesar de estos desafíos, concluye que el ritmo de avance es vertiginoso y que la comunidad de Erdős está sirviendo como modelo pionero para integrar la IA en la investigación matemática formal.

The readings shared in Bluesky on 4 December 2025 are:

• Formal analysis of the sigmoid function and formal proof of the universal approximation theorem. ~ Dustin Bryant, Jim Woodcock, Simon Foster. #ITP #IsabelleHOL
• Lean4Less: Eliminating definitional equalities from Lean via an extensional-to-intensional translation. ~ Rishikesh Vaishnav. #ITP #LeanProver
• #Exercitium: Sin consecutivos repetidos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 3 December 2025 are:

• Simp, made simple. ~ Yaël Dillies Paul Lezeau. #ITP #LeanProver
• An introduction to formal real analysis (Lecture 23: Uniformity II: continuity). ~ Alex Kontorovich. #ITP #LeanProver #Math
• ‘Reverse mathematics’ illuminates why hard problems are (Researchers have used metamathematical techniques to show that certain theorems that look superficially distinct are in fact logically equivalent). ~ Ben Brubaker. #Math #CompSci
• Mathematics is hard for mathematicians to understand too. ~ Emily Riehl. #Math
• #Exercitium: Búsqueda en lista de listas de pares. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 2 December 2025 are:

• The machine translation of Landau’s analysis of foundations in Rocq. ~ Yue Guan, Yaoshun Fu, XiangTao Meng. #ITP #Rocq #Math
• Formalization of brownian motion in Lean. ~ Rémy Degenne, David Ledvinka, Etienne Marion, Peter Pfaffelhuber. #ITP #LeanProver
• Kimina Lean server: A high-performance Lean server for large-scale verification. ~ Marco Dos Santos et als. #ITP #LeanProver #LLMs
• ProofGym: Unifying LLM-based theorem proving across formal systems. ~ Xinrui Li et als. #ITP #LeanProver #IsabelleHOL #CoqProver #LLMs
• The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025. #AI #Math
• HERMES: Towards efficient and verifiable mathematical reasoning in LLMs. ~ Azim Ospanov et als. #ITP #LeanProver #LLMs
• How IT managers fail software projects (AI won’t solve IT’s management problems). ~ Robert N. Charette. #Software
• A formalization of functor quasi-categories in Lean 4. ~ Jack McKoen. #ITP #LeanProver #Math

The readings shared in Bluesky on 28 November 2025 are:

• Mathematical thinking isn’t what you think it is (The mathematician David Bessis claims that everyone is capable of, and can benefit greatly from, mathematical thinking). ~ Kelsey Houston-Edwards. #Math
• The curious case of broken theorems (Mathematics shouldn't survive logical errors—yet it does). ~ David Bessis. #Math #ITP #LeanProver
• #Exercitium: Problema de las puertas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 27 November 2025 are:

• An introduction to formal real analysis (Lecture 22: Uniformity). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Mathematics: the rise of the machines. ~ Yang-Hui He. #AI #ITP #Math
• #Exercitium: Llanuras de longitud dada. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 26 November 2025 are:

• Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. #ITP #IsabelleHOL #Math
• Introduction to functional programming. ~ Noam Zeilberger. #Haskell #FunctionalProgramming
• First-order data types and pattern-matching ~ Noam Zeilberger. #Haskell #FunctionalProgramming
• Higher-order functions and type classes. ~ Noam Zeilberger. #Haskell #FunctionalProgramming
• Lambda calculus and typing. ~ Noam Zeilberger. #Haskell #FunctionalProgramming #LambdaCalculus #TypeTheory
• #Exercitium: Expresiones vectoriales. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 November 2025 are:

• Formalizing computational paths and fundamental groups in Lean. ~ Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras. #ITP #LeanProver
• REAL-Prover: Retrieval augmented lean prover for mathematical reasoning. ~ Ziju Shen et als. #ITP #LeanProver #LLMs #Math
• MiniF2F in Rocq: Automatic translation between proof assistants (A case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge. #AI #Math #ITP #Rocq #LeanProver #IsabelleHOL #LLMs
• Software never fails. ~ kqr. #Programming
• #Exercitium: Expresiones aritmética normalizadas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 24 November 2025 are:

• An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. #ITP #LeanProver #Math
• A perspective on interactive theorem provers in Physics. ~ Joseph Tooby-Smith. #ITP #LeanProver #Physics
• ITP 2025 Lean workshop. #ITP #LeanProver
• Gödel mirror: A paraconsistent calculus mechanized in Lean 4. ~ Jhet Chan. #ITP #LeanProver #Logic #Math
• Automatic geometry theorem proving using polynomial elaboration. ~ Mauricio Barba da Costa et als. #ITP #LeanProver #Math
• A topological rewriting of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. #ITP #CoqProver
• A Coq-based axiomatization of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. #ITP #CoqProver
• Set theory with types. ~ Lawrence Paulson. #Logic #Math #CompSci #SetTheory #TypeTheory
• A new bridge links the strange math of infinity to computer science. ~ Joseph Howlett. #Math #CompSci
• Tableau methodology for propositional logics. ~ T. Jarmuzek, R. Gore. #Logic

The readings shared in Bluesky on 23 November 2025 are:

• DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof
• Verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda
• Formalization of derived categories in Lean/mathlib. ~ Joël Riou. #ITP #LeanProver
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver
• A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van De Velde, Andrew Yang. #ITP #LeanProver #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• Testing a priority queue with Monolith. ~ François Pottier. #OCaml #FunctionalProgramming
• Reseña de «DeepMind’s latest: An AI for handling mathematical proofs». #AI #Math #ITP #LeanProver #AlphaProof

En el artículo «DeepMind’s latest: An AI for handling mathematical proofs», se presenta a AlphaProof, un sistema de inteligencia artificial capaz de razonar y realizar demostraciones matemáticas complejas. En la Olimpiada Internacional de Matemáticas de 2024, el sistema alcanzó el nivel de un medallista de plata, quedándose a un solo punto de obtener el oro.

El desafío del razonamiento lógico

Históricamente, los ordenadores han sido excelentes calculando, pero mediocres "entendiendo" la lógica necesaria para las demostraciones matemáticas. Los modelos de lenguaje actuales (como ChatGPT) funcionan mediante estadística y predicción de palabras, lo que a menudo resulta en respuestas que "suenan" bien pero son matemáticamente incorrectas. Para solucionar esto, DeepMind necesitaba un sistema que garantizase certeza absoluta.

Cómo funciona: La combinación de tres elementos

Para lograr este hito, AlphaProof combinó varias estrategias:

• Lenguaje formal (Lean): Utilizaron Lean, un software que permite escribir y verificar demostraciones matemáticas. Como había pocos datos de entrenamiento en este formato, usaron una versión de Gemini para traducir millones de problemas de lenguaje natural a Lean.

• Aprendizaje por refuerzo (Estilo AlphaZero): Emplearon una arquitectura similar a la que domina el ajedrez o el Go. Una red neuronal aprende mediante prueba y error, recompensando las demostraciones correctas y elegantes, combinada con un algoritmo de búsqueda en árbol para explorar posibles pasos lógicos.

• Aprendizaje en tiempo de prueba (TTRL): Esta es la gran innovación. Ante un problema muy difícil, la IA genera variaciones del mismo (algunas más simples, otras más generales) para "practicar" y aprender sobre la marcha, emulando cómo un humano intenta resolver versiones simplificadas de un problema antes de atacar el original.

Resultados

AlphaProof logró resolver el problema más difícil de la competición (el sexto), algo que solo consiguieron 6 de los 609 participantes humanos. En conjunto con AlphaGeometry 2 (que se encargó de un problema de geometría para el que AlphaProof no estaba optimizado), el sistema sumó 28 puntos.

Las limitaciones: Tiempo y coste

A pesar del éxito, el sistema tiene desventajas significativas frente a los humanos:

• Recursos desproporcionados: Mientras que los estudiantes tienen 4,5 horas por sesión, AlphaProof tardó días en resolver los problemas, utilizando una inmensa potencia de cálculo (cientos de días de procesamiento TPU).

• Coste prohibitivo: Actualmente, el coste de ejecutar este sistema es inviable para la mayoría de los investigadores.

• Dependencia humana: Los problemas tuvieron que ser traducidos manualmente a Lean antes de que la IA pudiera procesarlos.

El futuro

El objetivo de DeepMind no es ganar concursos como la IMO, sino optimizar esta tecnología para que sea menos costosa y pueda contribuir a la investigación matemática profesional, ayudando a descubrir nuevos conceptos en lugar de solo resolver los ya conocidos.

The readings shared in Bluesky on 20 November 2025 are:

• Formalization of Auslander-Buchsbaum-Serre criterion in Lean4. ~ Naillin Guan, Yongle Hu. #ITP #LeanProver #Math
• On small functions (and Haskell). ~ Alexander Przemysław Kamiński. #Haskell #FunctionalProgramming
• Hyperfunctions: Communicating continuations. ~ Donnacha Oisín Kidney, Nicolas Wu. #Haskell #FunctionalProgramming
• #Exercitium: Acrónimos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 19 November 2025 are:

• An introduction to formal real analysis (Lecture 20: Limits and continuity of functions). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Structuring definitions in mathematical libraries. ~ Alena Gusakov, Peter Nelson, Stephen Watt. #ITP #LeanProver #Math
• Pre*: The predecessors of a regular language w.r.t. a context-free grammar, with applications (in Isabelle/HOL). ~ Tassilo Lemke, Tobias Nipkow. #ITP #IsabelleHOL
• 10 developer habits that separate good programmers from great ones. ~ TheBitForge. #Programming
• #Exercitium: Particiones de longitud fija. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 November 2025 are:

• Teaching real analysis as a game. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Are automated proof assistants ready for semigroup research? Orientation-preserving mappings and proof assistant Lean. ~ Alastair Litterick, Alexei Vernitski, Billy Woods. #ITP #LeanProver #Math
• Lispy sets in CHICKEN Scheme. ~ Peter Bex.f#page=36 #Scheme #FunctionalProgramming
• Evaluating autoformalization robustness via semantically similar paraphrasing. ~ Hayden Moore, Asfahan Shah. #AI #Math #Autoformalization #ITP #LeanProver
• «Paged Out!»: una revista en PDF sobre programación, donde con un artículo por página sobra. ~ @Alvy #Programming
• Universidad e Inteligencia Artificial: realidad, retos y expectativas de la aplicación de la IA en las universidades españolas. ~ Teodoro Luque, Lucia Porcu, Isamel García Varea y Iñaki Fuertes Tudanca. #IA #Universidad
• #Exercitium: Evaluación de árboles de expresiones aritméticas. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 17 November 2025 are:

• An introduction to formal real analysis (Lecture 19: The rearrangement theorems). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formalizing neural networks (in Isabelle/HOL). ~ Achim D. Brucker, Amy Stell. #ITP #IsabelleHOL #NeuralNetwork
• xeus-haskell: a Jupyter kernel for Haskell based on the native implementation of the Jupyter protocol xeus. ~ Masaya Taniguchi. #Haskell #FunctionalProgramming
• #Exercitium: Aplicaciones alternativas. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 16 November 2025 are:

• To have machines make math proofs, turn them into a puzzle. ~ John Pavlus. #AI #Math #ATP #SatSolvers
• SITA: A framework for structure-to-instance theorem autoformalization. ~ Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen. #AI #Math #Autoformalization #LLMs #ITP #LeanProver
• #Exercitium: Repetición cíclica. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 14 November 2025 are:

• An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. ~ Nicolas Chappe et als. #ITP #Rocq
• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #CoqProver
• Towards type-directed compiler calculation. ~ Wouter Swierstra. #ITP #Agda
• Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. #ITP #Agda
• Checking equivalence in a non-strict language. ~ John Charles Kolesar, Ruzica Piskac, William Triest Hallahan.7#supplementary-materials #Haskell #FunctionalProgramming
• Automatically testing console I/O behavior of student submissions in Haskell. ~ Oliver Westphal, Janis Voigtländer. #Haskell #FunctionalProgramming
• Parallel dual-numbers reverse AD. ~ Tom J. Smeding, Matthijs I.L. Vákár. #Haskell #FunctionalProgramming
• Domain-specific tensor languages. ~ Jean-Philippe Bernardy, Patrik Jansson. #Haskell #FunctionalProgramming
• Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #Haskell #FunctionalProgramming
• Experiences of early assessment to teach functional programming. ~ Peter Chapman. #Haskell #FunctionalProgramming
• You could have invented Fenwick trees. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Patterns and paradoxes: The logic of pattern synonyms. ~ Koz Ross. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 49: Shrinking. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 50: Singletons. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 51: Typed servers using sop-core. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Tail recursion modulo context: An equational approach. ~ Daan Leijen, Anton Felix Lorenzen. #OCaml #FunctionalProgramming
• How we achieved an IMO medal, one year before any other AI system. ~ Tom Zahavy. #AI #Math #ITP #LeanProver #AlphaProof
• Olympiad-level formal mathematical reasoning with reinforcement learning. ~ Thomas Hubert et als. #AI #Math
• Reseña de «Olympiad-level formal mathematical reasoning with reinforcement learning». #AI #Math #ITP #LeanProver #AlphaProof
• #Exercitium: Cuantificadores sobre listas. #Haskell #ProgramaciónFuncional

En el artículo «Olympiad-level formal mathematical reasoning with reinforcement learning» se presenta AlphaProof, un agente de IA que utiliza aprendizaje por refuerzo para resolver problemas matemáticos complejos en el asistente de pruebas Lean. Combina una red neuronal con búsqueda en árbol para encontrar demostraciones formalmente verificables.

El sistema fue entrenado con millones de problemas auto-formalizados y emplea una innovadora adaptación en tiempo de prueba para los problemas más difíciles. Demostró capacidades excepcionales resolviendo problemas de competiciones como la Olimpiada Internacional de Matemáticas.

En la IMO 2024, AlphaProof resolvió tres problemas no geométricos, incluyendo el más difícil. Combinado con AlphaGeometry 2, el sistema logró una puntuación equivalente a medalla de plata, marcando un hito en el razonamiento matemático automatizado.

The readings shared in Bluesky on 13 November 2025 are:

• Computer-assisted proofs in Lean4. ~ J. Nijholt. #ITP #LeanProver #Math
• De la disputatio a la IA: regreso a los orígenes (La universidad como lugar de diálogo). ~ Neila Campos. #AI #Education
• #Exercitium: Inversa a trozos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 10 November 2025 are:

• Apriori knowledge in an era of computational opacity: The Role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math
• #Exercitium: Mínimos locales. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 9 November 2025 are:

• Towards formalizing reinforcement learning theory. ~ Shangtong Zhang. #ITP #LeanProver
• The philosophical prospects of Large Language Models in the future of mathematics. ~ Fenner Stanley Tanswell, Ásgeir Berg. #AI #Math

The readings shared in Bluesky on 8 November 2025 are:

• A new paradigm for mathematical proof? ~ Emily Riehl. #AI #Math #ITP #Agda #LeanProver
• An introduction to formal real analysis (Lecture 17: Series and convergence). ~ Alex Kontorovich. #ITP #LeanProver #Math
• #Exercitium: Pequeño test de inteligencia. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 7 November 2025 are:

• An introduction to formal real analysis (Lecture 16: Completeness of the real numbers). ~ Alex Kontorovich. #ITP #LeanProver #Math
• The path to a superhuman AI mathematician. ~ Lawrence Fisher. #AI #Math #ITP #LeanProver
• Math reasoning in times of AI: Lean way of theorem proving. ~ Jan Cepika et als. #ITP #LeanProver #Math #AI #LLM
• Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. #ITP #LeanProver #Rocq
• ScenicProver: A framework for compositional probabilistic verification of learning-enabled systems. ~ Eric Vin et als. #ITP #LeanProver
• Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. #ITP #Agda #HoTT
• Mathematical exploration and discovery at scale. ~ Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, Adam Zsolt Wagner. #AI #Math #AlphaEvolve #ITP #LeanProver
• It’s the specification, stupid! (Seeking a significant shift in the traditional software development and verification paradigm). ~ Manfred Broy, Harald Ruess, Natarajan Shankar. #FormalVerification
• ¿Cuál es el siguiente término? ~ Miguel Ángel Morales. #Matemáticas
• #Exercitium: Mayores elementos de una matriz. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 5 November 2025 are:

• Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #ITP #LeanProver #Math
• Tree-based premise selection for Lean4. ~ Zichen Wang, Anjie Dong, Zaiwen Wen. #ITP #LeanProver #AI
• #Exercitium: Conjunto de primos relativos. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Repetición de elementos. #Haskell #ProgramaciónFuncional
• #Exercitium: Último dígito no nulo del factorial. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 4 November 2025 are:

• Is this the end of handwritten math? Introducing Lean. ~ Ank Yog. #ITP #LeanProver #Math
• Quel sera l’impact de l’IA sur les mathématiques dans les prochaines années? - Timothy Gowers. #AI #Math #ITP #LeanProver

The readings shared in Bluesky on 2 November 2025 are:

• "Why don't you use dependent types?" ~ Lawrence Paulson. #ITP #Automath #LCF #IsabelleHOL #LeanProver #TypeTheory
• Lean4Physics: Comprehensive reasoning framework for college-level Physics in Lean4. ~ Yuxin Li et als. #ITP #LeanProver #Physics #AI #LLM
• On graded coeffect types for information-flow control. ~ Vilem-Benjamin Liepelt et als. #ITP #Agda
• Property-based testing for asynchronous functional reactive programming using linear temporal logic. ~ Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 1 November 2025 are:

• An introduction to formal real analysis (Lecture 15: The real numbers). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formalization of coverage checking in Agda. ~ Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe. #ITP #Agda #FunctionalProgramming
• Call-by-value and call-by-name: A simple proof of a classic theorem. ~ D. Biernacki, J. McKinna, & F. Sieczkowski. #ITP #Adga #FunctionalProgramming
• #Exercitium: Precio total. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 31 October 2025 are:

• Virasoro algebra and Sugawara constructions formally in Lean. ~ Kalle Kytölä. #ITP #LeanProver #Math
• Derivation of fundamental physical constants from substrate ontology. ~ Matthew Scherf. #ITP #LeanProver #Physics
• Conjecture extraction for proof autoformalization. ~ Simon Sorg, Wenda Li, Soumya Banerjee. #AI #Math #ITP #LeanProver #Autoformalization
• Accelerating discovery with the AI for Math Initiative (The initiative brings together some of the world's most prestigious research institutions to pioneer the use of AI in mathematical research). ~ Pushmeet Kohli, Eugénie Rives. #AI #Math
• GenAI for computing careers: A sunny take (Positive outcomes for computer science graduates will take some determined action from both educators and learners). ~ Saurabh Bagchi. #GenAI #CompSci #Education
• #Exercitium: Extensión de un fichero. #Haskell #ProgramaciónFuncional

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