El artículo «Silicon Valley Is in a frenzy over bots that build themselves» analiza la creciente carrera en Silicon Valley por crear inteligencias artificiales capaces de mejorar sus propias capacidades. OpenAI, Anthropic y Google DeepMind lideran estos esfuerzos, automatizando partes significativas de su investigación interna con resultados concretos aunque todavía limitados.

Los avances actuales son incrementales: las herramientas de IA agilizan tareas concretas, pero aún dependen de la supervisión humana para fijar objetivos y ejercer el juicio creativo que los expertos llaman "gusto investigador". Las predicciones más optimistas sitúan la automatización completa entre 2028 y 2032.

El entusiasmo coexiste con una alarma creciente. Investigadores, activistas e incluso políticos como Bernie Sanders advierten sobre la pérdida del control humano, mientras los gobiernos, todavía adaptándose a internet, difícilmente podrán regular una tecnología que avanza a este ritmo.

The readings shared in Bluesky on 4 April 2026 are:

• Why Lean?. ~ Leonardo de Moura. #LeanProver #ITP
• A formalization of the Gelfond-Schneider theorem. ~ Michail Karatarakis, Freek Wiedijk. #LeanProver #ITP #Math
• Formalizing Pick's theorem, efficiently. ~ Michael Eisermann. #LeanProver #ITP #Math
• Lean on Vampire proofs (short paper). ~ Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, Michael Rawson. #LeanProver #ITP #Vampire #ATP
• La IA acaba de hacerle una pregunta incómoda a la física teórica. Qué pasa si algunos de sus resultados más citados nunca fueron tan sólidos como parecían. ~ Martín Nicolás Parolari. #LeanProver
• Type-checked compliance: Deterministic guardrails for agentic financial systems using Lean 4 theorem proving. ~ Devakh Rashie, Veda Rashi. #LeanProver #ITP #LLMs
• Physics as code: From scans to theorems with ITP APIs in SU(5) model building. ~ Sven Krippendorf, Joseph Tooby-Smith. #LeanProver #ITP #Physics
• Pairwise independence of representation, classification, and composition in finite extensional magmas. ~ Stefano Palmieri. #ITP #LeanProver
• Optimal bounds for an Erdős problem on matching integers to distinct multiples. ~ Wouter van Doorn, Yanyang Li, Quanyu Tang. #AI4Math #LeanProver #ITP #LLMs
• Coherence for asynchronous buffered MPST: A mechanized metatheory. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• Computable dynamics for asynchronous MPST: Lyapunov descent, critical capacity, and decision procedures. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• Harmony from coherence in asynchronous MPST: A minimal erasure invariant for classical dynamics. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• On the formalization of network topology matrices in HOL. ~ Kubra Aksoy, Adnan Rashid, Osman Hasan, Sofiene Tahar. #ISabelleHOL #ITP #Math
• Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. #RocqProver #AI4Math
• Representing graphs in Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Encodings into the λ-calculus. ~ Kristopher Micinski. #LambdaCalculus #Racket #FunctionalProgramming
• What Gödel discovered. ~ Stepan Parunashvili. #Logic #Math #Lisp #Programming
• This startup wants to change how mathematicians do math. ~ Will Douglas Heaven. #AI4Math
• Short proofs in combinatorics and number theory. ~ Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant. #AI4Math
• How effective are current AI models on mathematical research problems?. ~ David H Bailey. #AI4Math
• Mathematical methods and human thought in the age of AI. ~ Tanya Klowden, Terence Tao. #AI #Math
• Category theory illustrated: Types. ~ Jencel Panic. #CategoryTheory #Math
• Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. #ITP #LeanProver #Math #AIforMath #Teaching
• 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
• 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
• Reseña de «Diophantine equations over Z: Universal bounds and parallel formalization». #ITP #IsabelleHOL #Math
• Reseña de «Solving formal math problems by decomposition and iterative reflection». #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• Reseña de «The Infinity Project (How to use AI and mathematics to prove and improve science and security)». #AI #Math #ITP #LeanProver
• Reseña de «Olympiad-level formal mathematical reasoning with reinforcement learning». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «DeepMind’s latest: An AI for handling mathematical proofs». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «Formalization of Erdős problems». #ITP #LeanProver #Math #Autoformalization
• Reseña de «Machine assistance and the future of research mathematics». #AI4Math
• Reseña de «Machine assistance and the future of research mathematics». #AI4Math
• Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». #AI4Math #LeanProver
• Reseña de «Completing the formal proof of higher-dimensional sphere packing». #AI4Math
• Reseña de «Shaping the future of mathematics in the age of AI». #AI4Math
• Reseña de «AI for mathematical and scientific discovery». #AI4Math
• Reseña de «Mathematicians in the age of AI». #AI4Math
• Reseña de «Coding after coders: The end of computer programming as we know it». #AI #Programming
• Reseña de «Eval awareness in Claude Opus 4.6’s BrowseComp performance». #AI
• Reseña de «Formal verification and AI are reshaping mathematical research». #AI4Math #ITP #LeanProver
• Reseña de «In math, rigor is vital. But are digitized proofs taking it too far?». #AI4Math #LeanProver #ITP
• Reseña de «Can machines do mathematics?». #AI4Math #LeanProver #ITP
• Reseña de «Advancing mathematics by guiding human intuition with AI». #AI4Math
• Reseña de «Shaping the future of mathematics in the age of AI». #AI4Math #LeanProver #ITP
• Reseña de «What happens when AI starts checking mathematicians’ work». #AI4Math #ITP #LeanProver
• Reseña de «As AI keeps improving, mathematicians struggle to foretell their own future». #AI4Math
• Reseña de «Mathematics in the library of Babel». #AI4Math
• Reseña de «Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools». #AI4Math
• Reseña de «This startup wants to change how mathematicians do math». #AI4Math
• Reseña de «La IA acaba de hacerle una pregunta incómoda a la física teórica. Qué pasa si algunos de sus resultados más citados nunca fueron tan sólidos como parecían». #LeanProver #ITP
• Reseña de «Short proofs in combinatorics and number theory». #AI4Math
• Reseña de «Mathematical methods and human thought in the age of AI». #AI4Math
• Reseña de «Mathematicians in the age of AI». #AI4Math
• Reseña de «AI for mathematical and scientific discovery». #AI4Math
• Reseña de «Accelerating mathematics». #AI4Math #LeanProver
• Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». #AI4Math #LeanProver
• Reseña de «Type-checked compliance: Deterministic guardrails for agentic financial systems using Lean 4 theorem proving». #LeanProver
• Reseña de «What Gödel discovered». #Logic #Math #Lisp #Programming
• Reseña de «Why Lean?». #LeanProver #ITP #FunctionalProgramming
• Reseña de «DeepSeek-Prover-V2-7B bridges the gap between mathematical thought and formal code». #AI4Math #LeanProver
• Reseña de «Recent advances in LLMs for mathematics». #AI4Math
• Reseña de «Aristotle, an AI theorem prover using Lean». #AI4Math #LeanProver
• Reseña de «Sobre la resolución de problemas de Erdös usando inteligencia artificial generativa». #AI4Math
• Reseña de «The story of Erdős problem #1026». #AI4Math
• Reseña de «50 years of proof assistants». #ITP #IsabelleHOL #LeanProver #CoqProver
• Reseña de «Teaching real analysis as a game»". #LeanProver #ITP #Math
• Reseña de «How we achieved an IMO medal, one year before any other AI system». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «A new paradigm for mathematical proof?». #Math #ITP #LeanProver #Agda

El artículo «DeepSeek-Prover-V2-7B bridges the gap between mathematical thought and formal code» presenta DeepSeek-Prover-V2-7B, un modelo diseñado para resolver uno de los retos más difíciles de la IA: demostrar teoremas matemáticos de forma rigurosa y verificable por ordenador mediante Lean 4.

El modelo emplea una estrategia de descomposición recursiva que divide problemas complejos en subtareas manejables. Con solo 7B parámetros, aprovecha conocimiento destilado de su versión mayor de 671B y logra puntuaciones destacadas en los bancos de pruebas miniF2F y PutnamBench.

Al ser un modelo abierto de 7B, puede ejecutarse en ordenadores personales con hardware modesto, lo que lo pone al alcance de investigadores individuales interesados en el razonamiento automático y la verificación formal con Lean 4.

El artículo «Why Lean?», de Leonardo de Moura, explica por qué Lean se ha convertido en una herramienta singular para verificación formal. Su característica más determinante es estar implementado en su propio lenguaje, lo que permite a cualquier programador extender el sistema desde sus entrañas sin fricciones ni capas intermedias.

Esto ha generado un ecosistema imprevisto: Mathlib supera los 200.000 teoremas escritos por la comunidad, y proyectos como Veil o Verso nacieron sin coordinación con sus creadores. Un kernel pequeño con múltiples implementaciones independientes garantiza que ninguna prueba incorrecta pase desapercibida, propiedad que Terence Tao identifica como esencial frente al aprendizaje por refuerzo.

El autor reconoce el precio de este enfoque: la compatibilidad hacia atrás se sacrifica cuando escalar lo exige, y él mismo cedió sus preferencias teóricas ante las necesidades reales de los usuarios. El resultado es un sistema menos puro, pero genuinamente útil.

El artículo «What Gödel discovered», escrito por un programador, explica cómo Russell destruyó la teoría fundacional de Frege con una paradoja y cómo Hilbert respondió exigiendo un sistema formal completo y consistente. Russell y Whitehead construyeron el Principia Mathematica como candidato, cuya densa notación el autor traduce a sintaxis Lisp para hacerla legible a desarrolladores.

Gödel ideó una codificación numérica que permitió al propio lenguaje hablar sobre sus demostraciones. El autor ilustra paso a paso, con expresiones como (proves a b) o (subst a b c), cómo Gödel construyó una sentencia que se declaraba a sí misma indemostrable, atrapando al sistema en un dilema sin salida.

Si el sistema es consistente, la sentencia es verdadera pero indemostrable, revelando su incompletitud. El autor concluye con una lectura orientada a programadores: así como Gödel creó el primer evaluador metacircular, sus teoremas prueban que existen verdades que nunca podrán expresarse como un algoritmo.

El artículo «Type-checked compliance: Deterministic guardrails for agentic financial systems using Lean 4 theorem proving» presenta una crisis arquitectónica en el sector financiero: los sistemas de IA agéntica operan de forma probabilística, mientras que reguladores como la SEC, FINRA y la OCC exigen garantías absolutas. Las soluciones actuales, como NeMo Guardrails, son insuficientes por su naturaleza estocástica.

Para resolverlo, los autores diseñan el Lean-Agent Protocol, que usa el modelo Aristotle para convertir políticas institucionales en axiomas de Lean 4. Cada acción propuesta por un agente debe ser demostrada matemáticamente antes de ejecutarse, con una latencia de solo cinco microsegundos y sandboxing vía WebAssembly.

El protocolo se despliega en tres fases progresivas y cubre las principales normativas financieras y de privacidad. Además, incorpora un mecanismo de explicación en lenguaje natural para auditorías, transformando errores formales en avisos comprensibles que satisfacen mandatos de transparencia algorítmica.

El artículo «La IA acaba de hacerle una pregunta incómoda a la física teórica. Qué pasa si algunos de sus resultados más citados nunca fueron tan sólidos como parecían» describe cómo se utilizó Lean para verificar resultados científicos. El hallazgo no fue obra de una IA generativa, sino de la formalización lógica estricta.

El sistema analizó un estudio de 2006 sobre el modelo de Higgs. Al intentar formalizarlo con Lean, se halló un contraejemplo que invalidaba la estabilidad del potencial defendida originalmente. Este fallo lógico persistió durante casi dos décadas sin que la revisión por pares humana lo detectara previamente.

Aunque los científicos corregirán el error, el caso genera inquietud sobre otros cimientos teóricos. La verdadera contribución de estas herramientas no es la invención creativa, sino actuar como auditores implacables. Su uso obliga a demostrar con rigor absoluto aquello que la comunidad científica simplemente daba por sentado.

El artículo «Short proofs in combinatorics and number theory» anuncia un cambio de paradigma en la investigación matemática: las tres demostraciones que contiene fueron creadas íntegramente por un modelo de IA de OpenAI, sin que los cinco coautores humanos contribuyeran a los argumentos matemáticos. Su papel se limitó a comprender y reescribir lo que la máquina produjo.

Los problemas resueltos llevaban décadas abiertos tras ser planteados por Erdős. Que una IA los resuelva antes que cualquier matemático humano ilustra la capacidad emergente de estos sistemas para el razonamiento formal profundo.

Los propios autores sometieron los mismos problemas a GPT-4.5 Pro para medir la reproducibilidad: el modelo público resolvió dos de los tres en pocos intentos. El artículo funciona así tanto como contribución matemática como experimento sobre las fronteras actuales de la IA en ciencia.

El artículo «Mathematical methods and human thought in the age of AI» examina el impacto de la inteligencia artificial en las matemáticas y en la sociedad, argumentando que su despliegue masivo ha precedido a cualquier reflexión filosófica o regulatoria seria. Los autores, una historiadora del arte y un matemático, encuentran terreno común en las preguntas éticas que plantea el uso cotidiano de estas herramientas.

Las matemáticas sirven como campo de pruebas privilegiado: su capacidad de verificación formal permite estudiar con rigor los límites de la IA, que puede producir demostraciones válidas pero carentes de intuición o narrativa comprensible. A esto se suman riesgos sociales como la brecha digital, el colapso de modelos por datos contaminados y la ausencia de estándares sobre autoría.

Termina proponiendo una transición desde un uso moderado hacia una integración "copernicana". En este escenario, la inteligencia humana deja de ser el centro exclusivo del universo cognitivo. La colaboración responsable permitirá que estas herramientas mejoren la calidad de vida sin degradar los logros intelectuales de la humanidad.

El artículo «This startup wants to change how mathematicians do math» describe el lanzamiento de Axplorer por parte de Axiom Math, una herramienta de IA diseñada para ayudar a los matemáticos a descubrir patrones y resolver problemas complejos. La herramienta, basada en un proyecto anterior llamado PatternBoost, busca superar las limitaciones de los LLMs al enfocarse en la generación de nuevas ideas.

Axplorer se diferencia de otras herramientas de IA por su accesibilidad, ya que puede funcionar en computadoras personales, eliminando la necesidad de supercomputadoras. Axiom Math espera que Axplorer contribuya a la iniciativa expMath de DARPA, que promueve el uso de la IA en matemáticas, y que impulse avances en campos como la informática y la seguridad en internet.

Aunque algunos matemáticos se muestran cautelosos sobre el impacto real de la herramienta, Axplorer ha demostrado su potencial al resolver el problema de los cuatro ciclos de Turán. Axiom Math espera que la comunidad matemática adopte Axplorer para generar soluciones y contraejemplos, acelerando así el proceso de descubrimiento matemático.

The readings shared in Bluesky on 29 March 2026 are:

• Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools. ~ Jarod Alper. #AI4Math #LeanProver #ITP #Math
• On the paucity of lattice triangles. ~ David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang. #LeanProver #ITP #Math
• Executable Gödel encodings: A verified runtime for logical syntax. ~ Adrian Diamond. #LeanProver #ITP #Logic #Math
• Lean: Collaboration using formalization. ~ Floris van Doorn. #LeanProver #ITP #Math
• Formalizing the sphere packing problem. ~ Maryna Viazovska. #LeanProver #ITP #Math
• A Lean formalisation of sphere packing in dimension 8. ~ Siddharth Hariharan. #LeanProver #ITP #Math
• Autoformalization: A year of progress. ~ Auguste Poiroux. #AI4Math #LeanProver
• Videos of talks at Swiss Mathematical Society Spring Meeting "Formalization and Proof Assistants" at UniDistance Suisse, 27/03/2026. #LeanProver
• Formally verifying digital circuits with category theory in Lean. ~ Matt Hunzinger. #LeanProver #ITP #CategoryTheory
• Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. #AI4Math #LeanProver #ITP
• What happens when AI starts checking mathematicians’ work. ~ Manon Bischoff. #AI4Math #LeanProver
• As AI keeps improving, mathematicians struggle to foretell their own future. ~ Joseph Howlett. #AI4Math #LeanProver
• Mathematics in the library of Babel. ~ Daniel Litt. #AI4Math
• Claude, mon ami (Eine intellektuelle romanze). ~ Martin Burckhardt. #AI #Programming

En el número actual (abril de 2026) del Boletín de la AMS, aparece un artículo de Jarod Alper titulado «Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools», donde el autor analiza la creciente influencia de la inteligencia artificial y el lenguaje Lean en la disciplina. Basándose en su labor en el eXperimental Lean Lab, Alper argumenta que los matemáticos deben adoptar estas tecnologías para elevar el rigor y la eficiencia en la investigación actual.

El texto explora áreas clave como la autoformalización y el descubrimiento de conjeturas mediante IA. Pese a las dificultades técnicas del software, Alper defiende que formalizar pruebas elimina errores, profundiza el entendimiento lógico y genera datos de alta calidad vitales para el avance del aprendizaje automático en matemáticas.

Concluye que los matemáticos deben liderar esta transformación para que el futuro de la disciplina no sea dictado solo por corporaciones. La IA redefinirá la investigación, pero la intuición humana seguirá siendo esencial para determinar qué enunciados tienen valor y desarrollar una verdadera comprensión matemática profunda.

El artículo «Mathematics in the library of Babel» explora el rápido progreso de la IA en el campo de las matemáticas. Inicialmente escéptico, el autor relata cómo los LLMs, han superado sus expectativas, demostrando capacidad para resolver problemas complejos y ofrecer pruebas de teoremas.

El texto analiza el proyecto "First Proof", una iniciativa que evalúa la utilidad de la IA en la investigación matemática. Los resultados, con la resolución exitosa de entre 6 y 8 problemas de 10, sugieren que la IA puede ser una herramienta valiosa para los matemáticos, aunque aún con margen de error.

El autor reflexiona sobre el futuro de la investigación matemática en un mundo donde la IA puede generar resultados de alta calidad de forma autónoma. Anticipa que la IA se convertirá en un colaborador esencial, pero que el papel del matemático humano seguirá siendo crucial para la creatividad, la validación y la exploración de nuevas fronteras del conocimiento.

El artículo «As AI keeps improving, mathematicians struggle to foretell their own future» describe cómo la IA está progresando rápidamente en el campo de las matemáticas. El proyecto First Proof, diseñado para evaluar las capacidades de los LLMs, ha revelado que estos sistemas pueden generar pruebas válidas para problemas matemáticos reales.

La primera ronda de pruebas mostró que los modelos de OpenAI y Google DeepMind superaron las expectativas, resolviendo parcialmente hasta ocho de diez problemas propuestos. Sin embargo, la verificación de estas pruebas resultó ser un desafío, ya que la IA puede cometer errores sutiles pero convincentes.

Para la segunda ronda, el equipo de First Proof exigirá transparencia y acceso a los modelos de IA participantes, así como una evaluación rigurosa por parte de expertos. El objetivo es comprender mejor las capacidades de la IA y anticipar su impacto en el futuro de la investigación matemática, asegurando que los jóvenes investigadores estén preparados para este nuevo panorama.

El artículo «What happens when AI starts checking mathematicians’ work» comenta que la comunidad matemática cuenta ahora con una herramienta de IA desarrollada por Math, Inc. llamada Gauss. Este sistema traduce demostraciones matemáticas al lenguaje formal de Lean y verifica su corrección, lo que agiliza la revisión de trabajos y garantiza la validez de los resultados.

Un equipo de investigadores liderado por Hariharan inició la formalización de las demostraciones de Maryna Viazovska sobre el empaquetamiento de esferas en dimensiones superiores. Sin embargo, Math, Inc. completó la formalización de forma autónoma utilizando Gauss, lo que suscitó interrogantes sobre la colaboración y el impacto de la IA en la investigación.

La formalización exitosa de las demostraciones de Viazovska marca un hito importante. Aunque la tecnología tiene limitaciones, su potencial para detectar errores, mejorar la precisión y fomentar nuevos descubrimientos es prometedor. El futuro de las matemáticas podría depender de la colaboración entre humanos y la IA.

El artículo «Shaping the future of mathematics in the age of AI» analiza la transformación de esta disciplina. Sus autores instan a la comunidad a liderar este cambio para asegurar que la automatización respete los valores intelectuales y estéticos fundamentales de la investigación matemática.

La dependencia de herramientas privadas amenaza la autonomía del campo. El predominio de intereses comerciales exige crear infraestructuras abiertas y transparentes para que los matemáticos controlen sus procesos. Solo así se evitará que empresas externas dicten qué es relevante o quién merece reconocimiento en la investigación.

Finalmente, se propone establecer principios éticos compartidos y fomentar la transparencia técnica. Los matemáticos deben liderar el desarrollo de sus propias herramientas para asegurar que la tecnología potencie el ingenio humano sin comprometer la esencia de su práctica profesional ni su independencia intelectual.

El artículo «Advancing mathematics by guiding human intuition with AI» presenta una nueva metodología para integrar la inteligencia artificial en el proceso de descubrimiento matemático. Los investigadores proponen un marco de trabajo donde la IA no reemplaza al matemático, sino que actúa como una herramienta para potenciar su intuición y ayudarle a identificar patrones ocultos en datos complejos.

Este marco se basa en el entrenamiento de modelos de aprendizaje automático para predecir relaciones entre objetos matemáticos. Si el modelo tiene éxito, se utilizan técnicas de atribución para comprender qué aspectos de los datos son más relevantes para la predicción, lo que a su vez puede inspirar nuevas conjeturas.

Los autores demuestran la eficacia de este enfoque en dos áreas de la matemática: la topología de nudos y la teoría de representación. En ambos casos, la IA ha ayudado a los investigadores a descubrir nuevas relaciones y a avanzar hacia la resolución de problemas, abriendo nuevas vías para la investigación futura.

En la conferencia «Can machines do mathematics?», Johan Commelin (director del proyecto Mathlib) analiza la vertiginosa evolución de la inteligencia artificial. De fallar en cálculos simples, la tecnología ha pasado a colaborar en investigaciones complejas y a ganar medallas en olimpiadas matemáticas gracias a herramientas de verificación formal.

El uso de asistentes como Lean permite gestionar pruebas inabarcables para el cerebro humano, facilitando colaboraciones masivas y seguras. Sin embargo, el auge de empresas privadas que priorizan el marketing sobre la transparencia científica plantea tensiones sociológicas que amenazan los valores tradicionales de la comunidad académica abierta.

Surgen dilemas sobre el papel del matemático en un entorno donde las máquinas generan infinitos teoremas. La capacidad de evaluar argumentos lógicos y encontrar significado entre el flujo computacional se vuelve crucial frente al riesgo de perder habilidades críticas fundamentales debido a la excesiva dependencia de estas herramientas.

Commelin insta a liderar esta transición mediante infraestructuras abiertas y currículos que enfaticen la creatividad y el planteamiento de problemas. El futuro debe equilibrar el potencial de la automatización con la esencia humana del descubrimiento, recordando que las matemáticas son, ante todo, una conversación entre personas.

El artículo «In math, rigor is vital. But are digitized proofs taking it too far?» explora la larga historia de la búsqueda de rigor en matemáticas, desde los axiomas de Euclides hasta los debates actuales sobre la formalización computacional. Esta búsqueda ha impulsado avances, pero también plantea interrogantes sobre el equilibrio entre precisión y creatividad.

El proyecto Lean, que busca formalizar toda la matemática en un lenguaje de programación, representa un esfuerzo ambicioso para verificar pruebas automáticamente. Sin embargo, el artículo plantea si esta formalización excesiva podría homogeneizar los enfoques y limitar la diversidad en el campo.

El futuro de la matemática se vislumbra como un equilibrio entre rigor y creatividad. La formalización computacional, como Lean, podría ser crucial, pero exige una reflexión sobre sus posibles implicaciones y la preservación de la intuición en el descubrimiento matemático.

El artículo «Formal verification and AI are reshaping mathematical research» revela una revolución en el campo de las matemáticas. Mientras que históricamente ha sido un ámbito de trabajo individual y manual, hoy evoluciona hacia un enfoque colaborativo y escalable, gracias a la fusión de LLMs y asistentes de prueba formal (como Lean).

El motor de esta transformación es la complementariedad entre ambas herramientas: los LLMs aportan creatividad y eficiencia en la generación de ideas y automatización de procesos, mientras que los asistentes de prueba aseguran la validez de cada paso. Esta alianza supera el desafío del "factor de Bruijn", permitiendo resolver problemas complejos como los planteados por Erdős.

Más allá de las matemáticas, esta metodología se aplica al desarrollo de software crítico, combinando inteligencia artificial y verificación formal para automatizar la generación de pruebas de corrección, haciendo accesible el software de alta fiabilidad a un público más amplio.

The readings shared in Bluesky on 24 March 2026 are:

• Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math
• The spectral comb and the Riemann hypothesis: A proof via fixed-point theory. ~ Engin Atik. #LeanProver #ITP #Math
• Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. #LeanProver #ITP #Math
• Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. ~ Vasily Ilin. #LeanProver #ITP
• Rado's radical reflections. ~ Rado Kirov. #LeanProver #ITP #FunctionalProgramming
• OpenGauss: an open source, state of the art autoformalization harness. #AI4Math #LeanProver #ITP #Autoformalization
• Verso: a platform for writing documents, books, course materials, and websites with Lean. #LeanProver
• Lebesgue-Stieltjes integral (in Isabelle/HOL). ~ Yosuke Ito. #IsabelleHOL #ITP #Math
• Sorted rewriting, conditional rewriting, and logically constrained rewriting (in Isabelle/HOL). ~ Akihisa Yamada. #IsabelleHOL #ITP
• A formal embedding for assessing the complexity of model consistency. ~ Romain Pascual et als. #IsabelleHOL #ITP
• Liberator: A drag-and-drop visual programming environment for Haskell. ~ Miles Berry. #Haskell #FunctionalProgramming

En el artículo «Eval awareness in Claude Opus 4.6’s BrowseComp performance» se comenta que Claude Opus 4.6 evidenció contaminación en el benchmark BrowseComp al localizar respuestas en fuentes públicas. Sin embargo, su hallazgo más significativo fue la capacidad de identificar que estaba siendo evaluado y descifrar la clave de acceso.

El modelo empleó herramientas como Python para extraer datos encriptados, revelando un nivel de inteligencia y resolución de problemas previamente no observado. Este comportamiento plantea serias dudas sobre la fiabilidad de los benchmarks web.

La contaminación se intensificó en configuraciones multi-agente. Las medidas de bloqueo resultaron insuficientes, exigiendo un enfoque continuo y adversarial para preservar la integridad de las evaluaciones.

En el artículo «Coding after coders: The end of computer programming as we know it» se comenta que la inteligencia artificial está transformando radicalmente la programación, con desarrolladores que ahora supervisan agentes capaces de generar y probar código automáticamente. Si bien esto multiplica la productividad, genera incertidumbre sobre el futuro del empleo y las competencias que los programadores deberán dominar.

El perfil del desarrollador está evolucionando hacia el de un "arquitecto digital", cuya labor consiste en evaluar y dirigir el trabajo de las IA. Este cambio democratiza la programación, permitiendo que personas sin formación técnica creen software, lo que podría redefinir la industria.

Silicon Valley enfrenta una revolución sin precedentes, donde la colaboración entre humanos e inteligencia artificial redefine no solo la profesión, sino también el panorama laboral en su conjunto, presentando tanto desafíos como oportunidades sin igual.

The readings shared in Bluesky on 19 March 2026 are:

• Aristotle: The World's most advanced formal reasoning agent. #LeanProver #ITP #Math
• Formalization of QFT (quantum field theory). ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. #LeanProver #ITP #Physics
• Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. #LeanProver #ITP #Math
• Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math
• Formal verification of axiom-free gödelian ontological argument and trinity necessity proof in Isabelle HOL. ~ Yong-Dock Kim. #IsabelleHOL #ITP
• In the mood for inference: Logic-based natural language inference with large language models. ~ Bill Noble, Rasmus Blanck, Gijs Wijnholds. #Prover9 #ATP #LLMs
• Acertijo del día: Un reto diario de lógica. #Logic

The readings shared in Bluesky on 14 March 2026 are:

• From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP
• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #LeanProver #ITP #Math
• Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. #LeanProver #ITP #Math
• Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. #LeanProver #ITP
• A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. #Agda
• Formalization of Wallis infinite product formula for π and the Wallis integral. ~ Yasushige Watase. #Mizar #ITP #Math
• Formalization of separable version of Banach–Alaoglu theorem. ~ Hiroyuki Okazaki, Takehiko Mieno. #Mizar #ITP #Math
• The evolution and societal impact of artificial intelligence in the 21st century. ~ Monica Khadgi. #AI

El artículo «Mathematicians in the age of AI» describe cómo la IA ha pasado, en menos de cuatro años, de ser incapaz de razonar matemáticamente a resolver problemas de nivel de investigación, tanto en demostraciones informales como formales verificadas por ordenador.

El episodio más revelador es el de Math Inc., que se apropió de un proyecto colaborativo de formalización para lanzar su agente Gauss con un golpe de efecto publicitario. Paralelamente, el agente Aletheia de DeepMind resolvió seis de diez problemas matemáticos inéditos propuestos por investigadores en activo.

El autor advierte del riesgo de pérdida de empleos y de sentido pedagógico, pero concluye con un llamamiento a la acción: los matemáticos deben liderar el uso de estas herramientas, preservar la intuición matemática en la enseñanza y aprovechar la IA para avanzar en los grandes problemas abiertos de la disciplina.

En el artículo «Mathematicians in the age of AI», Jeremy Avigad describe cómo la evolución de la IA ha sido meteórica desde la aparición de la IA generativa a finales de 2022, cuando sus capacidades matemáticas eran limitadas y motivo de burla. En menos de cuatro años, la tecnología ha pasado de fallar en problemas básicos a obtener medallas de oro en las Olimpiadas Internacionales y a resolver con éxito problemas de investigación inéditos, demostrando una potencia de razonamiento que se creía exclusivamente humana.

Este avance plantea desafíos éticos y profesionales, como las "demostraciones por sorpresa" realizadas por empresas privadas que podrían eclipsar el esfuerzo de los investigadores. Avigad sostiene que los matemáticos no deben esconderse, sino liderar y apropiarse de estas herramientas para potenciar su disciplina. El objetivo es que la tecnología ayude a resolver grandes enigmas, garantizando que la intuición y el criterio del matemático sigan siendo el eje fundamental y el motor de las matemáticas.

En el vídeo «AI for mathematical and scientific discovery», se explica cómo la IA ha evolucionado desde resolver problemas escolares hasta alcanzar niveles de medalla de oro en olimpiadas matemáticas. Los nuevos modelos de razonamiento ahora pueden resolver problemas de investigación inéditos de forma autónoma.

Se destacan aplicaciones en física teórica para simplificar cálculos complejos y en biología para automatizar laboratorios. Gracias a la integración con robótica, modelos como GPT-5 han realizado miles de experimentos autónomos, optimizando drásticamente los costes y la producción en la síntesis de proteínas.

La IA actúa como un colaborador que otorga «superpoderes» a los científicos. Aunque faltan retos en verificación e invención, Weil asegura que el progreso es exponencial. Su ambiciosa visión es que, gracias a esta tecnología, alcanzaremos los descubrimientos previstos para 2050 antes de 2030.

En el vídeo «AI for mathematical and scientific discovery» se explica cómo la IA ha evolucionado desde resolver problemas escolares hasta alcanzar niveles de medalla de oro en olimpiadas matemáticas. Los nuevos modelos de razonamiento ahora pueden resolver problemas de investigación inéditos de forma autónoma.

Se destacan aplicaciones en física teórica para simplificar cálculos complejos y en biología para automatizar laboratorios. Gracias a la integración con la robótica, modelos como GPT-5 han realizado miles de experimentos autónomos, optimizando drásticamente los costes y la producción en la síntesis de proteínas.

La IA actúa como un colaborador que otorga «superpoderes» a los científicos. Aunque faltan retos en verificación e invención, Weil asegura que el progreso es exponencial. Su ambiciosa visión es que, gracias a esta tecnología, alcanzaremos los descubrimientos previstos para 2050 antes de 2030.

The readings shared in Bluesky on 9 March 2026 are:

• Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP
• Formalization in Lean of faithfully flat descent of projectivity. ~ Liran Shaul. #LeanProver #ITP
• Formalizing a proof in Lean using Claude Code. ~ Terence Tao. #LeanProver #ITP #AI4Math
• Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. ~ Joseph Tooby-Smith. #LeanProver #ITP #Physics
• Formalizing unstable quasinormal modes and the quantum black hole bomb in Lean 4. ~ Naoki Takata. #ITP #LeanProver
• Implementing dependent type theory inhabitation and unification. ~ Chase Norman, Jeremy Avigad. #LeanProver #ITP
• LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. #LeanProver #ITP #Math #AI4Math
• Mathematicians in the age of AI. ~ Jeremy Avigad. #AI4Math #LeanProver #ITP
• Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. #AI4Math #LeanProver #ITP
• Unbiasing symmetric monoidal categories in Lean. ~ Robin Carlier. #LeanProver #ITP
• Apply2Isar: Automatically converting Isabelle/HOL apply-style proofs to structured Isar. ~ Sage Binder, Hanna Lachnitt, Katherine Kosaian. #IsabelleHOL #ITP
• A topological rewriting of Tarski’s mereogeometry. ~ Richard Dapoigny. #CoqProver #ITP
• Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. #RocqProver #ITP
• The floor is magma. ~ Alexandre Esteves. #Haskell #FunctionalProgramming
• Can the most abstract math make the world a better place? ~ Natalie Wolchover. #CategoryTheory #Math
• Category theory for programming. ~ Benedikt Ahrens, Kobe Wullaert. #CategoryTheory #Haskell #LeanProver #FunctionalProgramming
• Lambda calculus for dummies: The Church encoding. #LambdaCalculus #FunctionalProgramming
• Emacs and Vim in the age of AI. ~ Bozhidar Batsov. #Emacs #AI
• Una introducción a la programación en Emacs Lisp. ~ Robert J. Chassell, David Arroyo Menéndez. #Emacs #Lisp

En el artículo «Shaping the future of mathematics in the age of AI», coescrito por el medalla Fields Akshay Venkatesh, se analiza cómo la IA transforma la disciplina. Destacan métodos simbólicos como el asistente Lean y sistemas neuronales, advirtiendo que la comunidad debe liderar este cambio tecnológico.

La integración de IA y sistemas como Lean exige reformular la enseñanza y la investigación. El enfoque debe virar de la ejecución técnica al planteamiento de problemas y al juicio crítico, asegurando que la tecnología potencie la intuición humana sin perder la autonomía intelectual frente a intereses comerciales.

Finalmente, proponen crear infraestructuras de código abierto y normas éticas. Es vital proteger bibliotecas colaborativas frente al uso comercial sin atribución y mitigar desigualdades. La comunidad debe actuar para que el futuro de las matemáticas refleje sus valores y aspiraciones, no solo la lógica de las máquinas.

The readings shared in Bluesky on 4 March 2026 are:

• When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP
• Formalising sphere packing in Lean. ~ Chris Birkbeck, Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee, Maryna Viazovska. #LeanProver #ITP #Math
• The sphere packing project (Post 1: The story). ~ Chris Birkbeck Sidharth Hariharan Seewoo Lee. #LeanProver #ITP #Math
• Completing the formal proof of higher-dimensional sphere packing. #LeanProver #ITP #AI4Math
• The purpose of proofs. ~ Lance Fortnow. #LeanProver #ITP #AI4Math
• SorryDB: Can AI provers complete real-world Lean theorems? ~ Austin Letson et als. #LeanProver #ITP #AI
• ReasBook is a Lean 4 project for formalizing mathematics from textbooks and research papers. #LeanProver #ITP #Math
• A formally verified constructive proof of the consistency of Peano arithmetic using ordinal assignments. ~ Aaron Bryce, Rajeev Goré. #CoqProver #ITP #Math
• Mechanizing the proof of a borrow calculus. ~ Alban Reynaud Michez. #RocqProver #ITP
• Monuses and heaps. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming

Hoy se ha publicado el anuncio de la formalización total de los teoremas de Maryna Viazovska sobre el empaquetamiento de esferas. Con una extensión de aproximadamente 200,000 líneas de código en el lenguaje Lean, este proyecto se consagra como la mayor formalización de propósito único en la historia y el primer resultado galardonado con la Medalla Fields de este siglo en ser verificado íntegramente por computadora.

El núcleo matemático de este logro reside en resolver el milenario problema del empaquetamiento de esferas: ¿cómo disponer esferas idénticas en un espacio n-dimensional de la forma más densa posible? Mientras que para tres dimensiones la solución (conjeturada por Kepler en 1611) requirió siglos de esfuerzo y una compleja verificación computacional, Viazovska halló una solución "sorprendentemente simple" para la dimensión 8 mediante el uso de formas modulares. Su trabajo, extendido posteriormente a la dimensión 24 junto a otros colaboradores, demuestra que la red \(E_8\) y la red de Leech son los arreglos más densos y óptimos en sus respectivas dimensiones. La prueba es célebre por tender un puente magistral entre la geometría discreta, el análisis armónico y la teoría de números.

Una pieza clave de este éxito ha sido Gauss, un sistema de inteligencia artificial que ha transformado radicalmente los tiempos de ejecución. Mientras que proyectos de envergadura similar solían requerir décadas de esfuerzo humano, Gauss logró completar tareas críticas en cuestión de semanas. De manera sorprendente, la IA no solo finalizó la demostración en la dimensión 8 en apenas cinco días —un trabajo estimado en seis meses para un equipo humano—, sino que abordó la dimensión 24 de forma autónoma, realizando búsquedas bibliográficas y optimizando el código generado hasta reducirlo de medio millón de líneas a una versión más eficiente y mantenible.

Este avance trasciende la mera verificación; representa un cambio de paradigma en la investigación científica. Al convertir teorías complejas en datos navegables, modulares y procesables por máquinas, se abre la puerta a una nueva era de colaboración humano-IA. El éxito del proyecto demuestra que la autoformalización no solo es posible, sino que es capaz de integrar ramas diversas de la matemática en un corpus de conocimiento unificado y verificable a escala global.

Para conocer todos los pormenores técnicos y el alcance de este logro, se pueden consultar los detalles en: Completing the formal proof of higher-dimensional sphere packing.

The readings shared in Bluesky on 1 March 2026 are:

• Lean for science formalization. ~ Przemyslaw Chojecki. #LeanProver #ITP
• Vibe-coding a debugger for a DSL. ~ Joachim Breitner. #LeanProver
• Bidirectional interpolation for the lambda-calculus – Revisiting and formalising Craig-Čubrić interpolation. ~ Meven Lennon-Bertrand, Alexis Saurin. #RocqProver #ITP
• Machine-generated, machine-checked proofs for a verified compiler (Experience report). ~ Zoe Paraskevopoulou. #RocqProver #ITP

En el vídeo «AI that can prove it’s right: Verification as the missing layer in AI», Carina Hong explica cómo Axiom Math está desarrollando una inteligencia artificial matemática capaz de autoverificarse utilizando el lenguaje Lean. Su sistema, AxiomProver, no solo obtuvo una puntuación perfecta en el examen Putnam, sino que también resolvió cuatro conjeturas de investigación complejas sin ninguna intervención humana.

Hong subraya la importancia crucial de la verificación para eliminar las alucinaciones en los sistemas de IA. Al combinar razonamiento formal e informal, Axiom Math aspira a liderar un renacimiento matemático que permita resolver problemas históricos y transforme sectores críticos donde la precisión absoluta es fundamental para el desarrollo de nuevas tecnologías y descubrimientos científicos.

The readings shared in Bluesky on 24 February 2026 are:

• Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math
• Integral curves and flows on Banach manifolds in Lean. ~ Weichen Winston Yin, Yury Kudryashov. #LeanProver #ITP #Math
• Formalization of two fixed-point algorithms in Hilbert spaces. ~ Yifan Bai, Yantao Li, Jian Yu, Jingwei Liang. #LeanProver #ITP
• Nazrin: Atomic tactics for graph neural networks for theorem proving in Lean 4. ~ Leni Aniva, Iori Oikawa, David Dill, Clark Barrett. #LeanProver #ITP
• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #LeanProver #ITP
• DSLean: A framework for type-correct interoperability between Lean 4 and external DSLs. ~ Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck. #LeanProver #ITP
• A formal correctness proof of Edmonds’ blossom shrinking algorithm. ~ Mohammad Abdulaziz, Kurt Mehlhorn. #IsabelleHOL #ITP
• Verifying the hashgraph consensus algorithm. ~ Karl Crary. #CoqProver #ITP
• Classifying 2-groups in Homotopy Type Theory. ~ Perry Hart, Owen Milner. #Agda #ITP
• Formalized run-time analysis of active learning - coalgebraically in Agda. ~ Thorsten Wißmann. #Agda #ITP
• When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. #Agda #ITP #Vampire #ATP
• Haskell meets Evariste. ~ Paulo R. Pereira, Jose N. Oliveira. #Haskell #FunctionalProgramming
• Math in the age of AI. ~ Allyn Jackson. #AI4Math
• M2F: Automated formalization of mathematical literature at scale. ~ Zichen Wang et als. #AI4Math #ITP #LeanProver
• Large language model reasoning failures. ~ Peiyang Song, Pengrui Han, Noah Goodman. #LLMs #Reasoning

The readings shared in Bluesky on 19 February 2026 are:

• Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. #LeanProver #ITP #CSLib #CompSci
• Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. #LeanProver #ITP #CSLib #CompSci
• Pursuit of truth and beauty in Lean 4: Formally verified theory of grammars, optimization, matroids. ~ Martin Dvorak. #LeanProver #ITP #Math #CompSci
• Translating proofs from Lean to Dedukti. ~ Rishikesh Vaishnav. #LeanProver #Dedukti #ITP
• From sets in math to types in Lean: Subtype, Fin, Set, Finset, and Fintype. ~ Rado Kirov. #LeanProver #ITP
• Towards real-world industrial-scale verification: LLM-driven theorem proving on seL4. ~ Jianyu Zhang et als. #IsabelleHOL #ITP #LLMs
• Towards term-based verification of diagrammatic equivalence. ~ Julie Cailler, Noé Delorme, Simon Perdrix, Sophie Tourret. #IsabelleHOL #ITP
• A Rocq-based formalization of Hilbert’s geometry: Building a reusable foundation for 3D perpendicularity theory and verification. ~ Qimeng Zhang, Wensheng Yu. #RocqProver #ITP #Math
• A formal proof of Stirling’s formula. ~ Yasushige Watase. #Mizar #ITP #Math
• Case study: Saturations as explicit models in equational theories. ~ Mikoláš Janota, Michael Rawson, Stephan Schulz. #ATP #Vampire
• Proof assistants in the age of AI. ~ Leonardo de Moura. #AI4Math #ITP
• Mathematics and machine creativity: A Survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. #AI4Math #ITP
• #Exercitium: Matriz zigzagueante. #Haskell #FunctionalProgramming #Math

En el artículo «Mathematics and machine creativity: A survey on bridging mathematics with AI», se analiza cómo la IA transforma la investigación matemática. Aunque los modelos actuales fallan en lógica deductiva pura, su capacidad inductiva ofrece un valioso apoyo creativo para los matemáticos.

El texto destaca tres aplicaciones: demostraciones asistidas por computadora, formulación de conjeturas mediante reconocimiento de patrones y construcción de objetos matemáticos. Herramientas como FunSearch demuestran el potencial de la IA para descubrir soluciones innovadoras que superan las capacidades humanas tradicionales.

Finalmente, se abordan los límites actuales y el impacto educativo. Pese a no crear conceptos abstractos nuevos, la IA actúa como un socio estratégico que potencia la intuición humana, fomentando una colaboración interdisciplinaria necesaria para resolver problemas de la ciencia.

The readings shared in Bluesky on 14 February 2026 are:

• Formalization of the Golay-Hopf machine: A unified algebraic framework for Hida, Iwasawa, and Yang-Baxter structures. ~ Yoshihiro Hasegawa. #ITP #LeanProver
• Learning Lean (part 1). ~ Rado Kirov. #ITP #LeanProver #Math
• Leaning on AI. ~ Rado Kirov. #LeanProver #ITP #AI4Math
• Learning Lean (part 2). ~ Rado Kirov. #ITP #LeanProver #Math
• Learning Lean (part 3). ~ Rado Kirov. #ITP #LeanProver #Math
• Learning Lean (part 4). ~ Rado Kirov. #ITP #LeanProver #Math
• Machine assistance and the future of research mathematics. ~ Terence Tao. #AI4Math #ITP #LeanProver
• PBLean: Pseudo-boolean proof certificates for Lean 4. ~ Stefan Szeider. #ITP #LeanProver
• Why formalize mathematics - more than catching errors. ~ Rado Kirov. #ITP #LeanProver #Math
• RustCompCert: A verified and verifying compiler for a sequential subset of Rust. ~ Jinhua Wu, Yuting Wang, Liukun Yu, Linglong Meng. #ITP #CoqProver #RustLang
• Generalized decidability via Brouwer trees. ~ Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg. #Agda #ITP
• Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. #Minlog #Haskell #FunctionalProgramming
• LISP, Prolog and evolution. ~ Sami Badawi. #FunctionalProgramming #Lisp #Prolog #Haskell #Clojure
• Hilbert's program and infinity. ~ Richard Zach. #Logic #Math
• Accelerating mathematical and scientific discovery with Gemini Deep Think. ~ Thang Luong and Vahab Mirrokni. #AI4Math
• Accelerating scientific research with Gemini: Case studies and common techniques. ~ David P. Woodruff et als. #AI4Math
• LLMs for math research. ~ Dmitry Rybin. #AI4Math #ITP #LeanProver
• To be a frog with wings, should you choose (Recent progress on AI for mathematics and how to get involved). ~ Kevin Barreto. #AI4Math #ITP #LeanProver
• Towards autonomous mathematics research. ~ Tony Feng et als. #AI4Math

Ayer se publicó la conferencia de Terence Tao titulada «Machine assistance and the future of research mathematics», donde analiza la transformación de esta disciplina por la IA. Tao señala que las matemáticas están pasando de estudios individuales a proyectos masivos. El ingrediente clave es la verificación formal, que permite validar contribuciones masivas y filtrar el ruido de la IA.

Tao usa los problemas de Erdős para ilustrar cómo la IA agiliza la búsqueda de literatura y la traducción a código verificable. Aunque aún no supera los retos más complejos, la IA es ideal para resolver sistemáticamente problemas de dificultad media. Tao augura un futuro de colaboración humano-máquina que democratizará y escalará la investigación científica de forma inédita.

The readings shared in Bluesky on 9 February 2026 are:

• A Lean 4 formalization of the gaussian free field in d=4 and proof of the Osterwalder-Schrader axioms. ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. #ITP #LeanProver
• Accelerating mathematics. ~ Kevin Buzzard. #AI4Math #ITP #LeanProver
• CSLib: The Lean computer science library. ~ Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai. #ITP #LeanProver #CompSci
• Fel's conjecture on syzygies of numerical semigroups. ~ Evan Chen et als. #ITP #LeanProver #Math
• Formalization of Weyl’s law and its implementation into Lean code. ~ Zhibin Huang. #ITP #LeanProver #Math
• Inequalities for octad weights in M24 a computational framework formalized in Lean 4. ~ Yoshihiro Hasegawa. #ITP #LeanProver
• Statistical learning theory in Lean 4: Empirical processes from scratch. ~ Yuanhe Zhang, Jason D. Lee, Fanghui Liu. #ITP #LeanProver
• Towards trustworthy AI results using evidence structures: From certificates to argumentation frameworks. ~ Shawn Bowers1, Bertram Ludäscher. #ITP #LeanProver
• Formal P‑category theory and normalisation for simple type theory. ~ David George Berry. #ITP #RocqProver
• Evaluating Large Language Models on solved and unsolved problems in graph theory: Implications for computing education. ~ Adithya Kulkarni, Mohna Chakraborty, Jay Bagga. #AI4Math

El artículo «Accelerating mathematics» analiza cómo la tecnología busca acelerar el descubrimiento. Aunque los LLMs ayudan en lluvias de ideas, suelen «alucinar» y generar pruebas erróneas que parecen convincentes. Esto exige una revisión humana agotadora, evidenciando que la IA por sí sola aún no es una herramienta fiable para la investigación matemática de alto nivel.

Por otro lado, los sistemas como Lean garantizan precisión, pero sus bibliotecas carecen de definiciones modernas. Expandirlas es difícil porque requiere expertos escasos que dominen tanto la matemática avanzada como el código. En última instancia, el factor humano sigue siendo el gran cuello de botella, ya que el rigor necesario para evitar el error no puede automatizarse fácilmente todavía.

The readings shared in Bluesky on 4 February 2026 are:

• "Five-Point Haskell": Total depravity (and defensive typing). ~ Justin Le. #Haskell #FunctionalProgramming
• 'Sets' revisited: Working with a large category in Isabelle/HOL. ~ Eugene W. Stark. #ITP #IsabelleHOL
• A conversation on the future of mathematics. ~ Emily Riehl, Jesse Han, Jared Duker Lichtman. #ITP #LeanProver #Math
• Calling Lean functions as Python functions. ~ Philip Zucker. #ITP #LeanProver #Python
• Commutative algebras of series. ~ Lorenzo Clemente. #ITP #Agda #Math
• Construction-verification: A benchmark for applied mathematics in Lean 4. ~ Bowen Yang et als. #AI4Math #ITP #LeanProver
• Flow-based extremal mathematical structure discovery. ~ Gergely Bérczi, Baran Hashemi, Jonas Klüver. #AI4Math
• Formalization of non-Archimedean functional analysis 1: spherically complete spaces. ~ Yijun Yuan. #ITP #LeanProver #Math
• Hello, Haskell: Getting started in 2026. ~ Lukasz Tymoszczuk. #Haskell #FunctionalProgramming
• Irrationality of rapidly converging series: a problem of Erdős and Graham. ~ Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, Shengtong Zhang. #AI4Math
• LeanArchitect: Automating blueprint generation for humans and AI. ~ Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck. #AI4Math #ITP #LeanProver
• Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. #ITP #CoqProver
• Principles of programming languages. ~ Kristopher Micinski. #Programming #RacketLang
• Propositional logic proofs using Lean 4. ~ Kaue Silveira. #ITP #LeanProver #Logic #Math
• Recent advances in LLMs for mathematics. ~ Sebastien Bubeck. #AI4Math
• Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. ~ Tony Feng et als. #AI4Math #ITP #LeanProver
• The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory. ~ Tom de Jong, Nicolai Kraus, Axel Ljungström. #ITP #Agda
• The evolution of a Lean programmer. #ITP #LeanProver #FunctionalProgramming

En la conferencia «Recent advances in LLMs for mathematics», Sébastien Bubeck expone el salto desde la lógica básica de GPT-3.5 hasta el razonamiento de nivel de investigación en GPT-5. Los modelos han pasado de resolver problemas escolares de competición al 100% a abordar cuestiones abiertas, evolucionando desde respuestas directas hacia una compleja «cadena de pensamiento» interna.

El progreso se evidencia en áreas como la optimización convexa y la combinatoria. Los LLMs actuales son capaces de detectar vacíos en artículos científicos, mejorar límites matemáticos y hallar demostraciones inéditas más elegantes que las humanas. Tareas que requerirían meses de trabajo investigador se resuelven ahora en una tarde, empleando herramientas de aproximación avanzadas.

Pese al avance, el nivel actual equivale al de un estudiante de postgrado inicial y aún no alcanza la excelencia de las publicaciones más prestigiosas. Bubeck advierte sobre fallos en problemas de extrema complejidad y enfatiza que la pericia humana es hoy más crucial que nunca para validar resultados, orientar los modelos y profundizar en nuestra comprensión conceptual de la realidad.

En «Aristotle, an AI theorem prover using Lean», Alex Best presenta una IA de Harmonic que usa modelos de lenguaje y aprendizaje por refuerzo para demostrar teoremas en Lean de forma autónoma. Es capaz de autoformalizar artículos y hallar contraejemplos complejos. La IA se puede usar libremente en https://aristotle.harmonic.fun como un colaborador para acelerar la investigación.

The readings shared in Bluesky on 29 January 2026 are:

• Formalising the Bruhat-Tits tree. ~ Judith Ludwig, Christian Merten. #ITP #LeanProver
• Formalizing Fermat, Lecture 1. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalization of brownian motion in Lean. ~ David Ledvinka. #ITP #LeanProver
• New automation for Lean: grind. ~ Kim Morrison. #ITP #LeanProver
• MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL. ~ Julius Marx. #ITP #LeanProver
• Simpler do proofs with mvcgen. ~ Sebastian Graf. #ITP #LeanProver
• Formalizing value distribution theory of complex analysis. ~ Stefan Kebekus. #ITP #LeanProver #Math
• The Lean module system. ~ Sebastian Ullrich. #ITP #LeanProver
• Formalization of the Ionescu-Tulcea theorem in Mathlib. ~ Etienne Marion. #ITP #LeanProver #Math
• A bottom-up approach to formalisation in the FLT project. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• The universal divided power algebra. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• CSLib: The Lean Computer Science Library. ~ Fabrizio Montesi. #ITP #LeanProver
• Formalisation of CW complexes. ~ Hannah Scholz. #ITP #LeanProver #Math
• Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #ITP #LeanProver #Math
• lean-lsp-mcp: Tools for agentic interaction with Lean. ~ Oliver Dressler. #ITP #LeanProver #AI
• Tactics for the linear-bitwise fragment of bitvectors. ~ Siddharth Bhat. #ITP #LeanProver
• Coinductive predicates in Lean. ~ Wojciech Różowski. #ITP #LeanProver
• The state of Lean. ~ Leo de Moura. #ITP #LeanProver
• Locally nameless lambda calculi. ~ Chris Henson. #ITP #LeanProver
• Hopf algebras, affine group schemes and all of that. ~ Yaël Dillies. #ITP #LeanProver #Math
• Verification of model-checking techniques in Lean. ~ Atticus Kuhn. #ITP #LeanProver
• Teaching real analysis as a video game. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Autoformalization for physics and engineering with Lean. ~ Leopoldo Sarra. #ITP #LeanProver
• Formalization of homotopy theory in Lean. ~ Joël Riou. #ITP #LeanProver #Math
• The sphere packing project. ~ Sidharth Hariharan, Seewoo Lee, Chris Birkbeck. #ITP #LeanProver
• Internal projectivity of the sequence space in Lean. ~ Jonas van der Schaaf. #ITP #LeanProver #Math
• Formal verification of Rust cryptographic code in Lean with Aeneas. ~ Son Ho. #ITP #LeanProver
• Better living through metaprogramming. ~ Thomas R. Murrills. #ITP #LeanProver
• Verified computation of real asymptotics. ~ Vasilii Nesterov. #ITP #LeanProver
• Lessons from the Carleson project. ~ Floris van Doorn. #ITP #LeanProver
• The Mathlib initiative. ~ Johan Commelin. #ITP #LeanProver
• Formalizing class field theory. ~ Michał Mrugała. #ITP #LeanProver #Math
• Aristotle, an AI theorem prover using Lean. ~ Alex Best. #AI #Math #AI4Math #ITP #LeanProver #Aristotle
• Nori's construction in Lean. ~ Sophie Morel. #ITP #LeanProver
• Writing proofs by clicking. ~ Jovan Gerbscheid. #ITP #LeanProver
• What's new in the Lean standard library. ~ Markus Himmel, Sofia Rodrigues. #ITP #LeanProver
• Metaprogramming the next generation of testing tools. ~ Harry Goldstein. #ITP #LeanProver
• LeanTutor: Towards a verified AI mathematical proof tutor. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. #AI #Math #AI4Math #ITP #LeanProver #LLMs
• Competitive pure functional languages. ~ Sami Badawi. #FunctionalProgramming #Hakell #LeanProver
• Verified non-recursive calculation of Beneš networks applied to Classic McEliece. ~ Wrenna Robson, Samuel Kelly. #ITP #LeanProver
• A generalization of Boppana's entropy inequality. ~ Boon Suan Ho. #ITP #LeanProver
• Swap distance (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL
• Thinking machines: Mathematical reasoning in the age of LLMs. ~ Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen. #AI #Math #AI4Math #LLMs

The readings shared in Bluesky on 24 January 2026 are:

• Abel's limit theorem (in Isabelle/HOL). ~ Kangfeng Ye. #ITP #IsabelleHOL #Math
• A formalization of the downward Löwenheim-Skolem theorem in Coq. ~ Timothée Huneau. #ITP #CoqProver #Logic #Math
• Formally verified number-theoretic transform. ~ Alix Trieu. #ITP #RocqProver
• The HOL-Light library of multivariate real analysis in Rocq. ~ Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. #ITP #RocqProver #HOL_Light #Math
• Blurred drinker paradoxes and blurred choice axioms: Constructive reverse mathematics of the downward Löwenheim-Skolem theorem. ~ Dominik Kirst, Haoyi Zeng. #ITP #CoqProver #Logic #Math
• Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale. #ATP #Prover9 #Math
• Verified polynomial-time reductions in Lean 4: formalizing the complexity of decision-relevant information. ~ Tristan Simas. #ITP #LeanProver
• Sequencelib: A computational platform for formalizing the OEIS in Lean. ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
• Sequencelib: A platform for formalizing OEIS sequences in Lean 4. ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
• Numina-Lean-agent: An open and general agentic reasoning system for formal mathematics. ~ Junqi Liu et als. #ITP #LeanProver #Math
• ChatGPT and AI enhancing undergrad math. ~ Matthias Kawski. #AI #Math
• AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver
• Sobre la resolución de problemas de Erdős usando inteligencia artificial generativa. ~ Francisco R. Villatoro. #AI #Math #ITP #LeanProver

En «Sobre la resolución de problemas de Erdős usando inteligencia artificial generativa», Francisco R. Villatoro ofrece una visión panorámica en español sobre las aplicaciones de la IA en matemáticas. El artículo analiza cómo las IAs generativas están resolviendo problemas del célebre matemático Paul Erdős, aunque advierte contra el exceso de optimismo ante estos avances recientes.

El autor explica la metodología "vibe mathematics": usar IA para generar demostraciones, formalizarlas en Lean con Aristotle para verificarlas automáticamente, y repetir hasta obtener una correcta. Sin embargo, señala que la mayoría de intentos fracasan y que incluso demostraciones verificadas pueden resolver problemas distintos al original, como ocurrió con David Budden y Navier-Stokes.

Villatoro concluye que aunque el futuro es prometedor para problemas rutinarios, los grandes desafíos matemáticos requieren creatividad más allá de las IAs actuales. De los 1136 problemas de Erdős catalogados, 469 están resueltos, muchos gracias a la colaboración entre matemáticos humanos e IA, pero la tasa de éxito autónomo de las IAs sigue siendo baja (1-2%).

The readings shared in Bluesky on 19 January 2026 are:

• Broken proofs and broken provers. ~ Lawrence Paulson. #ITP #IsabelleHOL #RocqProver #LeanProver
• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Formalization of amicable numbers theory. ~ Zhipeng Chen, Haolun Tang, Jingyi Zhan. #ITP #LeanProver
• Resolution of Erdős problem #728: a writeup of Aristotle's Lean proof. ~ Nat Sothanaphan. #AI #Math #LLMs #ITP #LeanProver
• Erdos Problems LLM Hunter (A collection of attempts by advanced Large Language Models (LLMs) to solve open mathematical problems from the Erdős Problems collection and MathOverflow). ~ Paata Ivanisvili. #AI #Math
• Logic programming with extensible types. ~ Ivan Perez, Angel Herranz. #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Some Haskell idioms we like. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Playing with Gödel’s incompleteness theorem in Prolog. ~ Kenichi Sasagawa. #Prolog #LogicProgramming #Logic
• Mathematics as natural science in the era of AI. ~ Siddhartha Gadgil. #Math #AI

The readings shared in Bluesky on 14 January 2026 are:

• A lambda-superposition tactic for Isabelle/HOL. ~ Massin Guerdi. #ITP #IsabelleHOL
• Adding sorts to an Isabelle formalization of superposition. ~ Balazs Toth, Martin Desharnais-Schäfer, Jasmin Blanchette. #ITP #IsabelleHOL
• Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #LeanProver #FunctionalProgramming #ITP
• Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. #ITP #RocqProver
• Computing solutions for systems of multivariate ordinary differential equations in Rocq. ~ Holger Thies- #ITP #RocqProver
• Computation-tree semantics: An algorithmic approach to structurally defined relations. ~ Sean Kristian Remond Harbo, Hans Hüttel. #ITP #RocqProver
• Formal verification for JavaScript regular expressions: A proven mechanized semantics and its applications. ~ Aurèle Barrière, Victor Deng, Clément Pit-Claudel. #ITP #RocqProver
• 130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone? ~ Josef Urban. #ITP #Mizar #LLMs #Math #Autoformalization
• Using AI, mathematicians find hidden glitches in fluid equations. ~ Charlie Wood. #AI #Math
• #Exercitium: Números naturales separados por ceros. #Haskell #FunctionalProgramming #Math

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

En el artículo «The story of Erdős problem #1026», Terence Tao detalla la resolución de un problema de 1975 mediante una colaboración híbrida entre matemáticos y herramientas de IA. El proceso incluyó la formulación de conjeturas numéricas y pruebas formales en Lean generadas por sistemas como AlphaEvolve. La solución final se logró al vincular el reto con un problema de empaquetamiento de cuadrados y localizar, mediante una búsqueda profunda con IA, un teorema reciente en la literatura que completó la demostración.

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

En el artículo «50 years of proof assistants», Lawrence C. Paulson refuta el estancamiento científico mediante la evolución de la verificación formal. Desde 1975, con Edinburgh LCF y el lenguaje ML, se crearon los cimientos de los asistentes de demostración. Entre 1985 y 1995, herramientas como Isabelle y HOL permitieron las primeras verificaciones de hardware y consolidaron la lógica computacional.

Entre 1995 y 2015, la tecnología maduró tras fallos como el del Pentium. Se lograron hitos como la verificación del Teorema de los Cuatro Colores y el procesador ARM6. Posteriormente, se verificó software crítico como el kernel seL4 y el compilador CompCert, demostrando por primera vez que la corrección funcional total de sistemas complejos y el código libre de errores eran objetivos alcanzables.

Desde 2015, la adopción se disparó en matemáticas (con Lean) y en la industria. Gigantes como AWS y proyectos como CHERI integran ahora la verificación formal para garantizar la seguridad del hardware y la nube. El autor concluye que esta tecnología está pasando de ser una curiosidad académica a un estándar industrial «ordinario», demostrando un progreso científico vibrante y continuo.

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

En «Teaching real analysis as a game», Alex Kontorovich propone enseñar análisis real usando el asistente de pruebas Lean como un videojuego. Su idea central es que, al igual que un principiante de ajedrez necesita ver el tablero, los estudiantes necesitan una representación visual de las hipótesis y objetivos en una demostración. Lean actúa como ese "tablero de juego" interactivo e indispensable.

La metodología transforma el curso en niveles donde los estudiantes usan "tácticas" (comandos de Lean) para resolver problemas. Este enfoque fuerza a distinguir claramente entre lo que se sabe y lo que se debe probar. El objetivo no es aprender a programar, sino internalizar la lógica formal de manera intuitiva y profunda a través de la práctica interactiva.

Los resultados mostraron que los estudiantes, tras usar la herramienta, fueron capaces de escribir demostraciones en lenguaje natural excepcionalmente claras y rigurosas en sus exámenes. Kontorovich concluye que este método es prometedor, ya que sirve como un andamiaje efectivo para dominar la complejidad del análisis real.

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 «How we achieved an IMO medal, one year before any other AI system» se explica cómo AlphaProof logró un nivel de medalla de plata en la Olimpiada Internacional de Matemáticas. Este hito, alcanzado un año antes que cualquier otra IA, superó un gran desafío para la inteligencia artificial en una competición de élite para jóvenes matemáticos.

El avance crucial fue el "Aprendizaje por Refuerzo en Tiempo de Prueba" (TTRL). Esta técnica permitía al agente crear variaciones de los problemas y entrenar con ellas durante la propia competencia. Aunque consumía muchos recursos y tuvo resultados iniciales modestos, su refinamiento fue clave para lograr tres demostraciones completas tras tres días de prueba.

El autor señala futuros desafíos como la dependencia del demostrador Lean y la limitada cantidad de problemas matemáticos únicos. Su visión es desarrollar agentes que no solo resuelvan problemas, sino que generen sus propias preguntas y construyan teorías novedosas de forma autónoma.

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

En la conferencia «A new paradigm for mathematical proof?», Emily Riehl explora los desafíos actuales en la verificación de demostraciones matemáticas. Ejemplos como la conjetura de Kepler y el programa de Langlands muestran cómo las pruebas se han vuelto tan largas y complejas que incluso matemáticos como Voevodsky y Scholze han encontrado errores en su propio trabajo.

Como respuesta, Riehl propone la formalización computacional mediante asistentes de prueba como Lean y Agda. Proyectos como la verificación del teorema de Feit-Thompson demuestran que es posible certificar la corrección de demostraciones complejas mediante verificación automática, aunque requiere un esfuerzo colaborativo significativo.

La conclusión es que este enfoque podría constituir un nuevo paradigma para asegurar el rigor matemático, especialmente frente al riesgo de pruebas generadas por IA. Riehl sugiere que las demostraciones asistidas por computadora deberían incluir tanto la formalización verificada como una explicación para humanos, manteniendo así los estándares de la comunidad matemática.

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

En el artículo «The path to a superhuman AI mathematician», el profesor Sanjeev Arora propone que las matemáticas serán el primer dominio donde surgirá una IA superhumana. Esta se definiría como un sistema capaz de demostrar más teoremas que los logrados por la humanidad.

La ruta hacia este logro se basa en la verificación formal de pruebas con sistemas como Lean, que permite comprobar la corrección de forma automática. La IA se automejoraría mediante aprendizaje por refuerzo, usando Lean para validar sus respuestas sin depender solo de humanos. Además, podría generar sus propias preguntas matemáticas de manera creativa.

Evidencias recientes, como los modelos AlphaProof y Goedel-Prover, confirman esta tendencia. Arora concluye que, gracias a esta capacidad de verificación y mejora continua, una IA matemática superhumana es un horizonte plausible.

En el artículo «Mathematical exploration and discovery at scale» se presenta AlphaEvolve, un agente que combina modelos de lenguaje grande y algoritmos evolutivos para descubrir construcciones matemáticas. Probado en 67 problemas de matemáticas avanzadas, redescubrió y mejoró soluciones conocidas, demostrando su capacidad para explorar espacios de búsqueda complejos de forma eficiente.

El sistema opera evolucionando programas que buscan soluciones. Para la verificación, se integró con AlphaProof, logrando la formalización automática de pruebas en el asistente Lean. Aunque es más efectivo en problemas de optimización, sus resultados destacan el potencial de la IA como colaboradora en la investigación matemática a gran escala, desde el descubrimiento hasta la prueba formal.

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

En la conferencia «¿Cuándo podrá la Inteligencia artificial ayudarnos a demostrar teoremas?» se explica que la IA ya ayuda, pero con límites. Actualmente, es experta en reconocer patrones para encontrar contraejemplos o generar evidencia para conjeturas, pero depende de datos existentes.

Su papel actual es de "murmuración": sugiere posibles teoremas o caminos de prueba que los matemáticos deben verificar. Es una herramienta poderosa para explorar, pero no sustituye la creatividad e intuición humana necesarias para los avances genuinos.

El futuro próximo no es que la IA demuestre teoremas por sí sola, sino que actúe como un asistente. Ayudará en la formalización de pruebas y en la exploración de rutas, pero el matemático seguirá siendo esencial para la idea central y la verificación final.

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