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

The readings shared in Bluesky on 16 July 2025 are

• Formalization of derived categories in Lean/Mathlib. ~ Joël Riou. #ITP #LeanProver #Math
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• A complete formalization of Fermat’s Last Theorem for regular primes in Lean. ~ Alex J. Best et als. #ITP #LeanProver #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• A simple formalization of alpha-equivalence. ~ Kalmer Apinis, Danel Ahman. #ITP #Rocq
• Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #CoqProver
• LISA: A modern proof system. ~ Simon Guilloud, Sankalp Gambhir, Viktor Kunčak. #ITP #Lisa #Math
• #Exercitium: Problemas de programación con Haskell de febrero de 2021. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 15 July 2025 are

• Using Lean like an external SMT solver from Python. ~ Philip Zucker. #ITP #LeanProver
• IMO 1996 P3: Lean 4 formalization. ~ David Renshaw. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell de junio de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de mayo de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de abril de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de marzo de 2021. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 14 July 2025 are

• Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. #ITP #IsabelleHOL
• Quantifying bounded rationality: Formal verification of Simon's satisficing through flexible stochastic dominance. ~ Jingyuan Li, Zhou Lin. #ITP #LeanProver
• Could we teach ∞-category theory to undergraduates or to a computer? ~ Emily Riehl. #ITP #LeanProver #Math
• Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. #ITP #Coq
• Towards solving more challenging IMO problems via decoupled reasoning and proving- ~ Zhenwen Liang et als. #LLMs #ITP #LeanProver #Math

The readings shared in Bluesky on 13 July 2025 are

• Formalizing quasi-categories in Lean. ~ Jack McKoen. #ITP #LeanProver
• A simple AI chatbot (ChatGPT clone) built entirely in Haskell. ~ Tushar Adhatrao. #Haskell #FunctionalProgramming #LLMs

The readings shared in Bluesky on 12 July 2025 are

• A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. #ITP #CoqProver
• Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon #ATP #Prover9 #Math
• Proof theory and logic programming: Computation as proof search. ~ Dale Miller. #Logic #ProofTheory #LogicProgramming
• Teaching logic programming: a review. ~ Serhiy O. Semerikov et als. #LogicProgramming #Prolog #ASP #CLP
• Categorical semantics in Haskell. ~ Mohamed Amine Ayari. #Haskell #FunctionalProgramming #CategoryTheory
• Generic second-order matching, higher-order preunification and pattern unification - Implementations in Haskell. ~ Nikolai Kudasov et als. #Haskell #FunctionalProgramming
• CriticLean: Critic-guided reinforcement learning for mathematical formalization. ~ Zhongyuan Peng et als. #LLMs #ITP #LeanProver #Math
• ¿Por qué los usuarios de Emacs lo usan para todo? ~ Andros Fenollosa (2023). #Emacs

The readings shared in Bluesky on 11 July 2025 are

• Kimina-Prover: Applying test-time RL search on large formal reasoning models. ~ Haiming Wang et als. #LLMs #ITP #LeanProver
• AI for mathematical discovery (symbolic, neural and neuro-symbolic methods). ~ Moa Johansson. #AI #Math
• Cursos impartidos con materiales completos: apuntes, ejercicios y exámenes resueltos. #Lógica #ProgramaciónLógica #ProgramaciónFuncional #IA #RazonamientoAutomático

The readings shared in Bluesky on 10 July 2025 are

• The Haskell Unfolder Episode 46: Developing an application from scratch. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Curso "Razonamiento automático (2019-20)". #DemostraciónInteractiva #ProgramaciónFuncional #IsabelleHOL

The readings shared in Bluesky on 9 July 2025 are

• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• Doing Lean dirty: Lean as a Jupyter notebook replacement. ~ Philip Zucker. #ITP #LeanProver
• Robust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. #ITP #ACL2
• The φ-weighted recognition hamiltonian: A self-adjoint operator unifying automorphic L-functions, E 8 symmetry, and cosmic dynamics. #ITP #LeanProver
• Computational p-adics (in Isabelle/HOL). ~ Jeremy Sylvestre. #ITP #IsabelleHOL #Math
• The oneway to hiding theorem (in Isabelle/HOL). ~ Katharina Kreuzer, Dominique Unruh. #ITP #IsabelleHOL
• Kraus maps (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL
• Parikh's theorem (in Isabelle/HOL). ~ Fabian Lehr. #ITP #IsabelleHOL
• Computer-assisted proofs for differential equations and dynamical systems. ~ Maxime Breden. #ITP #Math
• Comparing codes: Binary search in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li et als. #SAT #CAS
• Bourbaki: Self-generated and goal-conditioned MDPs for theorem proving. ~ Matthieu Zimmer et als. #LLMs #ITP #LeanProver
• Clarifying before reasoning: A Coq prover with structural context. ~ Yanzhen Lu et als. #LLMs #ITP #CoqProver
• Curso "Lógica matemática y fundamentos (2019-20)". #Lógica #ProgramaciónFuncional #IsabelleHOL

The readings shared in Bluesky on 7 July 2025 are

• Lean: a theorem prover and programming language that enables correct, maintainable, and formally verified code. #ITP #LeanProver #FunctionalProgramming
• Curso "Razonamiento automático (2017-18)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Lógica matemática y fundamentos (2018-19)". #Lógica #ProgramaciónFuncional #IsabelleHOL
• Curso "Razonamiento automático (2018-19)". #DemostraciónInteractiva #ProgramaciónFuncional #IsabelleHOL #Coq
• Curso "Informática (2019-20)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2019-20). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2019-20). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2019-20). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 5 July 2025 are

• The filter game (in Lean 4). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formal verification of quantum stabiliser codes by stabiliser formalism. ~ Qiuyi Feng. #ITP #CoqProver
• Formal methods at NASA: Past, present, and future. ~ Paul Miner, Natasha Neogi. #FormalMethods #ITP #PVS
• A proof-assisted conversion of signal temporal logic formulas into negative normal form. ~ Danil Berrah, François Pessaux, Alexandre Chapoutot. #ITP #Rocq
• Functorial flattening of the state monad via vector‐space projection (A formally verified collapse model in Lean 4). ~ Jinu Jang. #ITP #LeanProver
• A diagrammatic calculus for a functional model of natural language semantics. ~ Matthieu Pierre Boyer. #Haskell #FunctionalProgramming
• Implementing a type theory with observational equality, using normalisation by evaluation. ~ Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami. #Haskell #FunctionalProgramming
• AI4Research: A survey of artificial intelligence for scientific research. ~ Qiguang Chen et als. #AI
• Curso "Informática (2018-19)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2018-19). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 4 July 2025 are

• LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving. ~ Naoto Onda et als. #ITP #LeanProver #Math #LLMs
• An introduction logical foundations of types and programming language. ~ Brigitte Pientka. #TypeTheory
• Reflections on Haskell and Rust. ~ Sibi Prabakaran. #Haskell #FunctionalProgramming #Rust
• Category theory: Introducing the perfect language. ~ Richard Southwell #CategoryTheory
• Reseña de «LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving». #ITP #LeanProver #Math #LLMs
• Curso "Razonamiento automático (2017-18)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Lógica matemática y fundamentos (2017-18)". #Lógica #IsabelleHOL

El campo de la demostración automática de teoremas se enfrenta a un obstáculo fundamental: a pesar del enorme potencial de los modelos de lenguaje para el razonamiento matemático, su progreso se ve frenado por la drástica escasez de datos de entrenamiento formales y de alta calidad. A diferencia de los vastos corpus de texto general, las bibliotecas matemáticas como Mathlib son relativamente pequeñas, lo que limita la capacidad de estos sistemas para aprender y mejorar.

Para resolver este desafío, en el artículo LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving se presenta una innovadora metodología para generar nuevas conjeturas de manera automática. El sistema adopta un enfoque híbrido: primero, extrae el contexto matemático (definiciones, variables) de un archivo de Lean existente, y luego utiliza un modelo de lenguaje exclusivamente para la tarea creativa de proponer nuevos enunciados de teoremas. Estas propuestas se someten a un proceso de filtrado iterativo para garantizar que sean sintácticamente correctas, novedosas y no triviales, alimentando las conjeturas válidas de nuevo al sistema para inspirar generaciones futuras cada vez más complejas.

El resultado es un éxito rotundo: el sistema no solo logra generar miles de conjeturas válidas y desafiantes, sino que demuestra su utilidad práctica al ser utilizadas para entrenar y mejorar el rendimiento de un demostrador de teoremas de vanguardia. Más allá de simplemente crear datos, LeanConjecturer fue capaz de formular y verificar teoremas genuinamente interesantes en el campo de la topología, estableciendo nuevas conexiones entre conceptos matemáticos. Con ello, el proyecto no solo ofrece una solución escalable al problema de la escasez de datos, sino que también abre una prometedora vía hacia la colaboración entre humanos y máquinas en el descubrimiento de nuevas matemáticas.

The readings shared in Bluesky on 3 July 2025 are

• LeanLTL: A unifying framework for linear temporal logics in Lean. ~ Eric Vin, Kyle A. Miller, Daniel J. Fremont. #ITP #LeanProver
• Verifying Datalog reasoning with Lean. ~ Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch. #ITP #LeanProver
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. #ITP #Agda

The readings shared in Bluesky on 1 July 2025 are

• Diophantine equations over Z: Universal bounds and parallel formalization. ~ Jonas Bayer, Marco David, Malte Hassler, Yuri Matiyasevich, Dierk Schleicher. #ITP #IsabelleHOL #Math
• Solutions to Tao's "Analysis I". ~ Dan Abramov. #ITP #LeanProver #Math
• The best new programming language is a proof assistant. ~ Harry Goldstein. #ITP #LeanProver
• Reseña de «Diophantine equations over Z: Universal bounds and parallel formalization». #ITP #IsabelleHOL #Math

Ayer se publicó un artículo que muestra el uso de la formalización con Isabelle en el desarrollo de la investigación matemática. Su título es Diophantine equations over Z: Universal bounds and parallel formalization y en sus conclusiones dice:

Nuestro proyecto demuestra que formalizar matemáticas altamente técnicas puede brindar beneficios reales, corrigiendo muchos errores mientras mejora la claridad y fiabilidad. El tiempo y esfuerzo adicional requeridos no pueden ignorarse, pero quedan compensados por las ventajas aquí expuestas.

En retrospectiva, identificamos dos factores clave que contribuyeron al éxito de este proyecto. En primer lugar, fue crucial apoyarnos en nuestra experiencia previa formalizando el ya consolidado teorema DPRM para tomar decisiones importantes en este proyecto. A quienes estén interesados en formalizar sus matemáticas, les recomendamos comenzar con un proyecto más pequeño cuyo objetivo sea formalizar un teorema ya establecido. En segundo lugar, fue de gran ayuda contar con un equipo interdisciplinario de personas con distintas habilidades. En nuestro caso, esto incluyó tanto a matemáticos puros como a informáticos, y fue su esfuerzo conjunto lo que permitió tender un puente desde las pruebas en lenguaje natural hasta el metalenguaje en el que está programado el propio Isabelle.

Fomentar que los matemáticos integren asistentes de prueba en su flujo de trabajo ahora ayudará a moldear el desarrollo de herramientas mejores, haciendo que la formalización en sistemas como Isabelle o Lean llegue a ser tan fluida como escribir en LaTeX. Esto se ve reforzado por los recientes avances en IA, que sugieren que pronto podrían surgir potentes herramientas de automatización para la formalización. Al formalizar las matemáticas ahora, aseguramos que nuestros campos se beneficien de la IA y la automatización a medida que estas herramientas evolucionen.

The readings shared in Bluesky on 30 June 2025 are

• Teaching children thinking. ~ Seymour A. Papert (1971). #CompSci #Teaching
• Curso "Lógica matemática y fundamentos (2016-17)". #Lógica #Haskell #ProgramaciónFuncional #IsabelleHOL
• Curso "Razonamiento automático (2016-17)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Informática (2017-18)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2017-18). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2017-18). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2017-18). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 29 June 2025 are

• Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL. ~ Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. #ITP #Rocq #Math
• Formal correctness proof of a mapping from a software specification language to the relational algebra. ~ Stan Dargent. #ITP #IsabelleHOL
• Functional programming (with some type theory) for metrology. ~ André Videla, Keith Lines. #Haskell #Idris #FunctionalProgramming
• Prover Agent: An agent-based framework for formal mathematical proofs. ~ Kaito Baba, Chaoran Liu, Shuhei Kurita, Akiyoshi Sannai. #LLMs #ITP #LeanProver
• Pearclustering: a novel clustering algorithm with an application to bike mobility. ~ Francisco Marquez-Saldaña, Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz. #AI
• Curso "Razonamiento automático (2014-15)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Informática (2015-16)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2015-16). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2015–16). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2015–16). #Haskell #ProgramaciónFuncional
• Curso "Lógica informática (2015-16). #Lógica #ProgramaciónLógica #Prolog
• Temas de "Lógica informática" (curso 2015-16). #Lógica #ProgramaciónLógica #Prolog
• Ejercicios de "Lógica informática" (curso 2015-16). #Lógica
• Curso "Lógica matemática y fundamentos (2015-16)". #Lógica #Haskell #ProgramaciónFuncional #IsabelleHOL
• Curso "Informática (2016-17)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2016-17). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2016-17). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2016-17). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 28 June 2025 are

• IsaBIL: A framework for verifying (in)correctness of binaries in Isabelle/HOL. ~ Matt Griffin, Brijesh Dongol, Azalea Raad. #ITP #IsabelleHOL
• Multiparty asynchronous session types: A mechanised proof of subject reduction. ~ Authors Dawit Tirore, Jesper Bengtson, Marco Carbone. #ITP #CoqProver
• Competitive programming in Haskell: prefix sums. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• ProofAug: Efficient neural theorem proving via fine-grained proof structure analysis. ~ Haoxiong Liu et als. #LLMs #ITP #IsabelleHOL #LeanProver
• Curso "Lógica informática (2014-15)". #Lógica #ProgramaciónLógica #Prolog
• Temas de "Lógica informática" (curso 2014-15). #Lógica #ProgramaciónLógica #Prolog
• Ejercicios de "Lógica informática" (curso 2014-15). #Lógica
• Curso "Lógica matemática y fundamentos (2014-15)". #Lógica #Haskell #ProgramaciónFuncional #IsabelleHOL

The readings shared in Bluesky on 27 June 2025 are

• Formalizing a proof in Lean by hand. ~ Terence Tao. #ITP #LeanProver #Math
• A formalization of the Ionescu-Tulcea theorem in Mathlib. ~ Etienne Marion. #ITP #LeanProver #Math
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Redefinitions in Mizar. ~ Alex Nelson. #ITP #Mizar #Math
• Position: Formal mathematical reasoning (a new frontier in AI). ~ Kaiyu Yang et als. #AI #LLMs #Math #AI4Math #ITP
• LOGICPO: Efficient translation of NL-based logical problems to FOL using LLMs and preference optimization. ~ Koushik Viswanadha, Deepanway Ghosal, Somak Aditay. #LLMs #Math #Autoformalization

The readings shared in Bluesky on 26 June 2025 are

• The correspondence between affine group schemes and Hopf algebras (in Lean). ~ Yaël Dillies, Michał Mrugała, Andrew Yang. #ITP #LeanProver #Math
• Searching for theorems in Mathlib. ~ Bolton Bailey. #ITP #LeanProver #Math
• The hidden number problem (in Isabelle/HOL). ~ Sage Binder, Eric Ren, Katherine Kosaian. #ITP #IsabelleHOL
• A modular splitting framework for saturation theorem proving (in Isabelle/HOL). ~ Ghilain Bergeron, Florent Krasnopol, Sophie Tourret. #ITP #IsabelleHOL
• The sigmoid function and the universal approximation theorem (in Isabelle/HOL). ~ Dustin Bryant, Jim Woodcock, Simon Foster. #ITP #IsabelleHOL
• Solving LinkedIn queens with Haskell. ~ Agnishom Chattopadhyay. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 45: Haskell records in 2025. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 25 June 2025 are

• Competitive programming in Haskell: range queries, classified. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Comparing codes: The sliding window in Haskell & Rust. ~ James Bowen. #Haskell #FunctionalProgramming #Rust

The readings shared in Bluesky on 23 June 2025 are

• Formalising differential geometry and topology in Lean: Differential forms and the Whitney–Graustein theorem. ~ Sam J. L. Lindauer. #ITP #LeanProver #Math
• A verified algebra of cognition: A Coq formalization of the distinction field. ~ Andrey Shkursky. #ITP #CoqProver
• A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL
• Towards advanced mathematical reasoning for LLMs via first-order logic theorem proving. ~ Chuxue Cao et als. #LLMs #ITP #LeanProver #Math
• Curso "Informática (2014-15)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima

The readings shared in Bluesky on 22 June 2025 are

• Conway’s normal form in the Mizar system. ~ Karol Pąk. #ITP #Mizar #Math
• Application of complex classes to number theory (in Mizar). ~ Rafał Ziobro. #ITP #Mizar #Math
• Free product of groups (in Mizar). ~ Sebastian Koch. #ITP #Mizar #Math
• Surreal numbers: A study of square roots (in Mizar). ~ Karol Pąk. #ITP #Mizar #Math
• Surreal dyadic and real numbers: A formal construction (in Mizar). ~ Karol Pąk. #ITP #Mizar #Math

The readings shared in Bluesky on 21 June 2025 are

• Theorem proving in Lean 4. ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich et als. #ITP #LeanProver
• Certifying projected knowledge compilation. ~ Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule. #ITP #HOL4
• Freer arrows and why you need them in Haskell. ~ Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li. #Haskell #FunctionalProgramming
• Property-based testing of attribute grammars. ~ José Nuno Macedo, Marcos Viera, João Saraiva. #Haskell #FunctionalProgramming
• Curso "Lógica informática (2013-14)". #Lógica #ProgramaciónLógica #Prolog
• Curso "Lógica matemática y fundamentos (2013-14)". #Lógica #Haskell #ProgramaciónFuncional #IsabelleHOL
• Curso "Razonamiento automático (2013-14)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 20 June 2025 are

• Lean won the SIGPLAN Programming Languages Software Award 2025. ~ Adolfo Neto. #ITP #LeanProver
• Theorems about abelian categories (in Lean). ~ Markus Himmel, Joël Riou. #ITP #LeanProver #Math
• Lean obtiene el prestigioso «SIGPLAN Programming Languages Software Award 2025». #ITP #LeanProver

El demostrador de teoremas Lean ha sido galardonado con el «SIGPLAN Programming Languages Software Award 2025», otorgado por ACM SIGPLAN (Special Interest Group on Programming Languages de la ACM (Association for Computing Machinery).

La cita del premio destaca lo siguiente:

El demostrador de teoremas Lean constituye un sistema informático extraordinario. Fundamentado en sólidas bases teóricas y de ingeniería, Lean ha ejercido y continúa ejerciendo un amplio impacto tanto en la práctica industrial como en la investigación científica.

El proyecto Lean ha generado un impacto particularmente significativo en tres áreas clave: matemáticas, verificación de hardware y software, e inteligencia artificial. En el ámbito matemático, ha logrado una aceptación considerable dentro de la comunidad académica, evidenciada por el desarrollo de Mathlib, una biblioteca creada por usuarios que supera las 1.8 millones de líneas de código.

La credibilidad del sistema se ha consolidado mediante la verificación exitosa de resultados fundamentales, incluyendo Liquid Tensor Experiment (propuesto por el medallista Fields Peter Scholze) y la verificación de la conjetura polinomial de Freiman-Ruzsa dirigida por el medallista Fields Terence Tao. Estos logros han proporcionado al sistema un reconocimiento sin precedentes en la comunidad científica internacional.

Es indiscutible que los métodos formales basados en Lean ocuparán una posición central en el desarrollo de las matemáticas durante los próximos años. Paralelamente, el sistema ha demostrado su valor práctico en proyectos industriales de verificación críticos, tales como la verificación del lenguaje de control de acceso Cedar en Amazon Web Services, la validación del muestreador SampCert para privacidad diferencial (también en AWS), y diversos proyectos de verificación blockchain en empresas líderes como StarkWare y Nethermind.

Finalmente, el éxito de iniciativas como AlphaProof de DeepMind y la adopción estratégica de Lean por parte de empresas emergentes como Harmonic han consolidado su posición como la solución de referencia para sistemas de razonamiento matemático potenciados por inteligencia artificial.

The readings shared in Bluesky on 19 June 2025 are

• Galois energy games (in Isabelle/HOL). ~ Caroline Lemke. #ITP #IsabelleHOL
• Chomsky-Schützenberger representation theorem (in Isabelle/HOL). ~ Moritz Roos. #ITP #IsabelleHOL
• Dyck language (in Isabelle/HOL). ~ Tobias Nipkow, Moritz Roos. #ITP #IsabelleHOL
• Making concurrent hardware verification sequential. ~ Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, Arvind. #ITP #CoqProver #Rocq
• Reviving DSP for advanced theorem proving in the era of reasoning models. ~ Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, Fan Yang. #AI #Math #AIforMath #LLMs #ITP #LeanProver
• Reseña de «Can A.I. quicken the pace of math discovery?». #AI #Math #AIforMath #ITP #LeanProver

El artículo «Can A.I. quicken the pace of math discovery?» presenta la iniciativa "Exponentiating Mathematics" de DARPA. Su objetivo es desarrollar una IA como coautor para acelerar la investigación en matemáticas.

El programa confronta limitaciones de los LLMs actuales. Estos fallan en razonamiento lógico-matemático y generan "alucinaciones". La solución propuesta integra IA con asistentes de prueba formales como Lean.

Lean desempeña el papel central como verificador. Los LLMs generan pruebas formales que Lean acepta o rechaza según su corrección. Esta iteración crea un ciclo de refinamiento continuo. Su lenguaje específico resulta arduo, pero su metodología es fundamental. La verificación formal garantiza corrección absoluta y elimina alucinaciones de LLMs generativos.

La meta es crear IA que sugiera ideas y construya pruebas verificadas. Los sistemas formales garantizan fiabilidad absoluta. Esto transforma herramientas actuales en colaboradores matemáticos confiables.

The readings shared in Bluesky on 17 June 2025 are

• LeanHammer: an automated reasoning tool for Lean which combines multiple techniques for proof search and formal reconstruction. ~ Joshua Clune et als. #ITP #LeanProver
• Monads are not like burritos. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Comparing codes: Two pointer algorithms. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Making GHCi compatible with multiple home units. ~ Hannes Siebenhandl, Matthew Pickering. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 16 June 2025 are

• 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
• LeanExplore: A search engine for Lean 4 declarations. ~ Justin Asher. #ITP #LeanProver
• An approach to formalize information-theoretic security of multiparty computation protocols. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Rocq
• Toward a formalization of secure multiparty computation stack. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikaaw. #ITP #CoqProver #Rocq

The readings shared in Bluesky on 15 June 2025 are

• BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. #ITP #CoqProver #Rocq #Math
• Introduction to competitive programming in Haskell. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Data structures and algorithms for competitive programming in Haskell. ~ Soumik Sarkar. #Haskell #FunctionalProgramming
• Hardest problems in mathematics, physics & the future of AI. ~ Terence Tao, Lex Fridman. #ITP #LeanProver #AI #Math #AIforMath
• Hablemos de LISP. ~ Manuel Rubio, Antonio Rubio. #Lisp #Programming
• Reseña de «Hardest problems in mathematics, physics & the future of AI». #ITP #LeanProver #AI #Math #AIforMath
• Reseña de «Hablemos de Lisp». #Lisp #FunctionalProgramming

El vídeo «Hablemos de Lisp» presenta un diálogo que explora la historia, conceptos fundamentales y legado duradero del lenguaje de programación Lisp. El análisis comienza con una perspectiva histórica rigurosa, desmitificando la creencia común de que fue el primer lenguaje funcional. En su lugar, identifica al IPL (Information Processing Language) de Herbert Simon y Allen Newell como su precursor fundamental.

Contexto histórico y pioneros

El vídeo establece una distinción crucial entre los diferentes pioneros de la inteligencia artificial: mientras que Simon y Newell sentaron las bases conceptuales del campo, John McCarthy acuñó el término "inteligencia artificial" y creó LISP, inspirado precisamente por las capacidades de procesamiento de listas que había demostrado IPL.

La naturaleza funcional de LISP

Respecto al paradigma funcional, el análisis revela que LISP, en sus primeras etapas, no cumplía estrictamente con los principios de la programación funcional moderna, como la inmutabilidad y la gestión explícita de efectos secundarios. La formalización teórica de este paradigma se atribuye posteriormente a la familia de lenguajes ISWIM, propuesta por Peter Landin.

Evolución técnica y conceptual

La génesis de la implementación de LISP se sigue de FLPL (Fortran Lisp Processing Language), un lenguaje intermedio que resultó fundamental por introducir la expresión condicional, una construcción sintáctica que más tarde sería adoptada ampliamente por lenguajes imperativos.

El momento decisivo: concepto versus implementación

Una de las discusiones más reveladoras del vídeo aborda la distinción entre el concepto original de LISP (1959) y su primera implementación (1960). McCarthy había concebido inicialmente una sintaxis de alto nivel (M-expresión) que se compilaría a una representación simbólica intermedia (S-expresión). Sin embargo, el éxito de la implementación de la función eval puso de manifiesto la profunda simetría entre código y datos —la homoiconicidad— inherente a la S-expresión.

Esta propiedad fundamental resultó tan poderosa que llevó al abandono de la M-expresión, convirtiendo la sintaxis intermedia en el lenguaje de programación definitivo.

Legado e influencia contemporánea

El vídeo concluye evaluando el legado perdurable de LISP en la ciencia de la computación. Se le atribuye la introducción de conceptos fundamentales como la expresión condicional y la recolección automática de basura (garbage collection). Su relevancia actual se manifiesta a través de sus numerosos dialectos modernos, destacando Common Lisp, Scheme, Clojure y Racket, que continúan explorando y expandiendo los principios originales del lenguaje.

En la entrevista "Hardest problems in mathematics, physics & the future of AI", Terence Tao comparte sus reflexiones sobre diversos problemas fundamentales sin resolver en análisis y teoría de números, examina la metodología de la investigación matemática contemporánea y analiza el papel emergente que desempeñan la verificación formal y la inteligencia artificial en la disciplina.

Problemas fundamentales y sus complejidades intrínsecas

Tao examina varios problemas que se encuentran en la frontera del conocimiento matemático actual. En análisis, dedica especial atención al problema de Kakeya, destacando sus profundas conexiones con el análisis armónico y las ecuaciones en derivadas parciales. Su análisis revela cómo este problema aparentemente geométrico se entrelaza con áreas fundamentales del análisis moderno.

Respecto al problema de la regularidad de Navier-Stokes, Tao identifica la "supercriticalidad" como el obstáculo central que impide su resolución. De manera particularmente innovadora, describe su construcción teórica de un análogo fluídico de una máquina de von Neumann, presentándola como una estrategia prometedora para demostrar la existencia de explosiones en tiempo finito (blowup) en las soluciones de estas ecuaciones.

Desafíos en teoría de números

En el ámbito de la teoría de números, Tao analiza la conjetura de los primos gemelos, atribuyendo su persistente dificultad a la extrema fragilidad del patrón subyacente. Explica cómo este patrón podría ser destruido por "conspiraciones" matemáticas imperceptibles para los métodos estadísticos tradicionales. Esta fragilidad contrasta marcadamente con la robustez inherente de las progresiones aritméticas, como las estudiadas en el teorema de Green-Tao.

Un concepto clave que emerge de su análisis es el problema de la paridad*, que identifica como un obstáculo metodológico fundamental en teoría de números. En cuanto a la hipótesis de Riemann, Tao la considera aún más inaccesible a los métodos actuales, situándola en una categoría propia de dificultad.

Marco filosófico y metodológico

Un hilo conductor de la entrevista es la exploración de la dicotomía entre estructura y aleatoriedad, un tema que permea múltiples áreas de las matemáticas. Esta perspectiva filosófica informa tanto el análisis de problemas específicos como la comprensión general de los fenómenos matemáticos.

Metodológicamente, Tao defiende un enfoque de simplificación estratégica en la resolución de problemas. Su estrategia consiste en descomponer problemas complejos en dificultades individuales, abordar cada una por separado, y posteriormente integrar las soluciones. Este método refleja una filosofía pragmática que prioriza la claridad conceptual y el progreso incremental.

Transformación tecnológica de las matemáticas

Una porción sustancial de la discusión se centra en el impacto transformador de la prueba asistida por ordenador, con particular énfasis en el asistente de pruebas Lean. Tao ilustra su potencial a través de su "Equational theories project" de clasificación de 22 millones de identidades algebraicas, demostrando cómo estas herramientas facilitan la colaboración a gran escala y la gestión de la complejidad en pruebas matemáticas modernas.

Sus predicciones sobre el futuro son especialmente significativas: anticipa que las herramientas de inteligencia artificial revolucionarán la formalización matemática. Más ambiciosamente, prevé que la IA podría generar conjeturas matemáticas genuinamente novedosas al identificar conexiones profundas entre campos aparentemente dispares.

Síntesis y perspectiva

La entrevista proporciona una ventana excepcional al proceso intelectual de uno de los matemáticos más influyentes de nuestra época. Tao logra equilibrar la precisión técnica con la accesibilidad conceptual, ofreciendo tanto análisis detallados de problemas específicos como reflexiones más amplias sobre la naturaleza de la investigación matemática.

Su visión integra consideraciones técnicas, marcos filosóficos y prospectivas tecnológicas, presentando una imagen completa de las matemáticas como disciplina en constante evolución. La entrevista destaca no solo los desafíos actuales, sino también las herramientas emergentes que podrían redefinir fundamentalmente cómo se desarrollarán las matemáticas en el futuro.

The readings shared in Bluesky on 14 June 2025 are

• Formalizing information theory in Lean 4: divergences, hypothesis testing and the data processing inequality. ~ Lorenzo Luccioli. #ITP #LeanProver #Math
• Collaboration and innovation in the Equational Theories Project: Formalizing mathematics with Lean 4. ~ Marco Petracci. #ITP #LeanProver #Math
• Is Emacs an operating system? #Emacs
• Curso "Razonamiento automático (2012-13)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Informática (2013-14)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima

The readings shared in Bluesky on 13 June 2025 are

• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Formal verification of relational algebra transformations in Fiat2 using Coq. ~ Christian Teshome. #ITP #CoqProver #Rocq
• Growing a modular framework for modal systems - HOLMS: a HOL Light library. ~ Antonella Bilotta. #ITP #HOL_Light #Logic #Math
• Trinity: an autoformalization system for verified superintelligence. #Autoformalization #AIforMath #ITP #LeanProver
• The abc conjecture almost always — autoformalized. ~ Jesse Michael Han et als. #Autoformalization #AIforMath #ITP #LeanProver
• MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Mathesis: Towards formal theorem proving from natural languages. ~ Yu Xuejun et als. #AI #LLMs #Math #ITP #LeanProver #AIforMath
• StepProof: Step-by-step verification of natural language mathematical proofs. ~ Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, Ivan Y. Tyukin. #LLMs #ITP #IsabelleHOL #Math #AIforMath
• Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Reseña de «Mathesis: Towards formal theorem proving from natural languages». #AI #LLMs #Math #ITP #LeanProver #AIforMath

En el artículo «Mathesis: Towards formal theorem proving from natural languages», se aborda la limitación clave de los demostradores de teoremas: su dependencia de enunciados ya formalizados. El trabajo se centra en el paso crítico de la 'autoformalización' —la traducción a un lenguaje formal como Lean 4— y presenta Mathesis, un sistema integral diseñado para automatizar todo el proceso.

El sistema introduce un Mathesis-Autoformalizer entrenado mediante aprendizaje por refuerzo para optimizar la traducción a código Lean. Su rendimiento se evalúa con LeanScorer, y se pone a prueba en Gaokao-Formal, un nuevo y exigente banco de pruebas. Finalmente, Mathesis-Prover genera la demostración completa en Lean, asegurando que la prueba final sea verificable.

Los resultados demuestran que Mathesis alcanza un rendimiento de vanguardia en varios bancos de prueba. El análisis revela una conclusión crucial: las mejoras en la autoformalización impactan el éxito final mucho más que las mejoras en el demostrador. Esto se explica porque si el problema se traduce incorrectamente a código Lean, el demostrador recibe una tarea mal planteada y no puede generar una prueba válida, sin importar su potencia. El trabajo confirma así que una traducción inicial de alta calidad es el factor más determinante para el éxito del proceso.

En el artículo «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?», los autores investigan la aplicabilidad de los modelos de lenguaje grandes multimodales (MLLMs) al problema de la demostración automática de teoremas que involucran componentes tanto textuales como visuales. Motivados por las limitaciones de los enfoques puramente textuales en dominios como la geometría, donde los diagramas constituyen información esencial, desarrollan un marco de evaluación sistemático para esta clase de problemas.

La contribución principal consiste en la construcción de MATP-BENCH, un conjunto de datos que contiene más de 1000 problemas matemáticos multimodales formalizados en tres asistentes de demostración: Lean 4, Coq e Isabelle/HOL. El corpus abarca problemas de complejidad variable, desde el nivel de secundaria hasta competiciones matemáticas avanzadas, proporcionando así un banco de pruebas comprehensivo para evaluar capacidades de razonamiento multimodal.

Los experimentos incluyen seis modelos representativos: tres con capacidades especializadas de razonamiento (OpenAI-o1, Claude-3.7-Sonnet-Thinking, Gemini-2.0-Flash-Thinking) y tres sin estas capacidades (GPT-4.1, Qwen2.5-VL-Instruct-70B, Llama3.2-Vision-Instruct-11B). Los resultados revelan que, si bien los modelos demuestran competencia en la comprensión de problemas y formalización de enunciados, exhiben deficiencias significativas en la construcción de cadenas de inferencia válidas.

El análisis establece que la principal limitación no radica en las capacidades de percepción visual sino en la insuficiencia del razonamiento simbólico formal. Los autores concluyen que los MLLMs actuales no constituyen demostradores automáticos efectivos para problemas multimodales, identificando la brecha entre comprensión multimodal y razonamiento lógico como el desafío fundamental a resolver.

MATP-BENCH se posiciona como el primer banco de prueba estándar para este dominio, proporcionando una base metodológica para la evaluación de futuros desarrollos en demostración automática multimodal.

The readings shared in Bluesky on 12 June 2025 are

• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• Lean meta-theory: The proofs behind the proofs. ~ Mario Carneiro. #ITP #LeanProver
• Litex: Scale formal reasoning in AI age. ~ Jiachen Shen. #Logic #ATP #LitexLang
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #ITP #LeanProver #LLMs
• Can large language models verify system software? A case study using FSCQ as a benchmark. ~ Jianxing Qin et als. #LLMs #ITP #CoqProver #Rocq
• Reinventing records and variants. ~ Murat Kasimov. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 11 June 2025 are

• LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. #ITP #LeanProver #Math #AIforMath #Teaching
• Common Lean pitfalls. ~ Niels Voss. #ITP #LeanProver
• Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library. ~ Brenda Potts. #ITP #LeanProver #RustLang
• Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. #Logic #SMT #Z3 #Teaching
• 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
• El futuro del razonamiento matemático: Integrando IA y Lean. #IA #ITP #LeanProver #Math #AIforMath
• Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. #ITP #LeanProver #Math #AIforMath #Teaching