The readings shared in Bluesky on 20 November 2025 are:
The readings shared in Bluesky on 19 November 2025 are:
The readings shared in Bluesky on 18 November 2025 are:
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:
The readings shared in Bluesky on 16 November 2025 are:
The readings shared in Bluesky on 14 November 2025 are:
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:
The readings shared in Bluesky on 10 November 2025 are:
The readings shared in Bluesky on 9 November 2025 are:
The readings shared in Bluesky on 8 November 2025 are:
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:
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:
The readings shared in Bluesky on 4 November 2025 are:
The readings shared in Bluesky on 2 November 2025 are:
The readings shared in Bluesky on 1 November 2025 are:
The readings shared in Bluesky on 31 October 2025 are:
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:
The readings shared in Bluesky on 29 October 2025 are:
The readings shared in Bluesky on 28 October 2025 are:
En el artículo de «Les IA vont-elles remplacer les mathématiciens?» se explora el rápido avance de la IA en matemáticas. Sistemas como Gemini o AlphaProof ya resuelven problemas de olimpiadas a nivel de medalla de oro y superan exámenes complejos. Este progreso, impulsado por entrenamiento masivo y nuevos modelos de razonamiento, plantea si podrán igualar la creatividad humana.
Sin embargo, el artículo matiza estos logros. Las IA aún son inconsistentes, cometen errores en problemas simples y carecen de la comprensión profunda y creatividad necesarias para la investigación de vanguardia. Expertos coinciden en que su pensamiento es mecánico y les falta la visión intuitiva para manejar conceptos matemáticos abstractos, necesitando posiblemente una nueva arquitectura.
El futuro no es de reemplazo, sino de colaboración. La IA se vislumbra como una herramienta poderosa que automatizará tareas tediosas, ayudará a verificar pruebas e incluso podrá sugerir nuevas líneas de investigación. Los matemáticos podrían usar estas herramientas para aumentar su productividad y explorar problemas de una manera antes imposible, transformando así la profesión.
En la conferencia «Gauss – towards autoformalization for the working mathematician», Jared Duker Lichtman presentó el proyecto Gauss, que busca automatizar la traducción de pruebas matemáticas a código formal verificable por máquina, haciendo esta práctica accesible para más matemáticos.
Como caso de estudio, se destacó la exitosa formalización automática de la versión "fuerte" del Teorema de los Números Primos en Lean. El agente Gauss generó 25.000 líneas de código en tres semanas, un hito de escala sin precedentes en la automatización.
El proyecto, que aún requiere un matemático en el bucle de retroalimentación, demuestra el potencial de estas herramientas para expandir y comprimir el conocimiento matemático de forma verificable, invitando a la comunidad a participar en esta visión futura.
The readings shared in Bluesky on 27 October 2025 are:
The readings shared in Bluesky on 26 October 2025 are:
The readings shared in Bluesky on 25 October 2025 are:
The readings shared in Bluesky on 24 October 2025 are:
The readings shared in Bluesky on 23 October 2025 are:
The readings shared in Bluesky on 22 October 2025 are:
Terence Tao ha comentado en Mastodon otro ejemplo interesante de la asistencia informática en matemáticas, que involucra nuevamente a los problemas de Erdös: el Problema #707, anteriormente marcado como "abierto", ahora está "refutado" - con la refutación formalizada en Lean. Pero el camino hacia esa refutación fue bastante inusual, y no encajaba perfectamente en ninguna de las narrativas estándar sobre la IA en las matemáticas.
La refutación inicial fue obra de humanos usando argumentos convencionales, sin ayuda inicial de LLMs. Sin embargo, descubrieron después que el problema ya había sido resuelto tres décadas antes por Hall, un hallazgo que las búsquedas bibliográficas humanas y asistidas por IA no detectaron. Para formalizar su prueba en Lean, los autores, sin experiencia previa, usaron ChatGPT en un proceso de "codificación por vibraciones", logrando generar unas 3000 líneas de código verificadas. Este proceso incluso permitió corregir un error en la formalización original del problema.
Este caso ilustra un uso muy específico y responsable de la IA: no para generar ideas matemáticas, sino para asistir en la creación de código formal verificable. La formalización complementa, pero no reemplaza, la prueba humana central. Debido a su contribución crucial en esta etapa, tanto ChatGPT como Lean aparecen como coautores del artículo, destacando un modelo inusual de colaboración humano-IA.
The readings shared in Bluesky on 21 October 2025 are:
The readings shared in Bluesky on 20 October 2025 are:
The readings shared in Bluesky on 18 October 2025 are:
En el artículo «Ax-Prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics» se presenta Ax-Prover, un sistema que combina modelos de lenguaje generales con el asistente de pruebas Lean. Este enfoque supera las limitaciones de los demostradores especializados, ofreciendo una solución más flexible y accesible para la verificación de teoremas.
La evaluación en dominios como álgebra abstracta y física cuántica demuestra que Ax-Prover supera significativamente a los modelos especializados. Además, probó su utilidad práctica al colaborar con un matemático en la verificación de un teorema complejo, completando el proceso en solo dos días e identificando un error en la prueba original.
The readings shared in Bluesky on 17 October 2025 are:
The readings shared in Bluesky on 16 October 2025 are:
The readings shared in Bluesky on 15 October 2025 are:
The readings shared in Bluesky on 14 October 2025 are:
The readings shared in Bluesky on 13 October 2025 are:
The readings shared in Bluesky on 11 October 2025 are:
The readings shared in Bluesky on 10 October 2025 are:
En el artículo «Mathematicians’ new best friend?», se analiza el impacto transformador de la inteligencia artificial en las matemáticas, a partir de una mesa redonda celebrada durante el 12º Foro de Laureados de Heidelberg, un encuentro internacional que reúne a jóvenes investigadores y destacados científicos. En este contexto, expertos debatieron cómo la IA ya acelera la resolución de problemas abiertos y podría incluso superar la creatividad humana en tareas como la formulación de conjeturas, lo que genera preocupación sobre el futuro del trabajo matemático. Aunque algunos comparan este cambio con actividades como el ajedrez —donde los humanos siguen participando pese a la superioridad de las máquinas—, otros subrayan que la comunidad matemática aún tiene la responsabilidad de guiar la integración de la IA para preservar el valor humano de la intuición, la interpretación y la creatividad en la disciplina.
The readings shared in Bluesky on 9 October 2025 are:
En «Mathematics: The rise of the machines», Yang-Hui He explora cómo la IA está transformando la investigación matemática, desde la verificación formal de teoremas y el descubrimiento de conjeturas hasta la resolución de problemas con modelos de lenguaje.
The readings shared in Bluesky on 8 October 2025 are:
The readings shared in Bluesky on 7 October 2025 are:
The readings shared in Bluesky on 6 October 2025 are:
The readings shared in Bluesky on 4 October 2025 are:
The readings shared in Bluesky on 03 October 2025 are:
The readings shared in Bluesky on 02 October 2025 are:
The readings shared in Bluesky on 01 October 2025 are:
The readings shared in Bluesky on 30 September 2025 are:
The readings shared in Bluesky on 29 September 2025 are:
The readings shared in Bluesky on 28 September 2025 are:
The readings shared in Bluesky on 26 September 2025 are:
The readings shared in Bluesky on 25 September 2025 are:
The readings shared in Bluesky on 24 September 2025 are:
The readings shared in Bluesky on 23 September 2025 are:
The readings shared in Bluesky on 22 September 2025 are:
The readings shared in Bluesky on 20 September 2025 are:
The readings shared in Bluesky on 19 September 2025 are:
The readings shared in Bluesky on 18 September 2025 are:
El artículo «Claude can (sometimes) prove it» comenta que Claude Code, el agente de IA de Anthropic, posee una capacidad sorprendente para la demostración interactiva de teoremas (ITP) en Lean, un campo reservado hasta ahora a expertos. Aunque no es totalmente autónomo y requiere supervisión humana para actuar como "gestor del proyecto", el agente puede descomponer tareas complejas, escribir definiciones, generar pruebas y refactorizar código. Su eficacia reside en la retroalimentación estricta de Lean, que le permite iterar y corregir errores. Pese a su lentitud y a algunos fallos conceptuales, supone un avance radical: acerca la verificación formal, antes prohibitiva por su complejidad, a un futuro donde podría ser accesible y automatizada.
The readings shared in Bluesky on 17 September 2025 are:
The readings shared in Bluesky on 15 September 2025 are:
The readings shared in Bluesky on 14 September 2025 are:
The readings shared in Bluesky on 13 September 2025 are:
The readings shared in Bluesky on 12 September 2025 are
The readings shared in Bluesky on 11 September 2025 are
The readings shared in Bluesky on 10 September 2025 are
The readings shared in Bluesky on 9 September 2025 are
The readings shared in Bluesky on 8 September 2025 are
The readings shared in Bluesky on 7 September 2025 are
The readings shared in Bluesky on 6 September 2025 are
The readings shared in Bluesky on 5 September 2025 are
The readings shared in Bluesky on 4 September 2025 are
The readings shared in Bluesky on 3 September 2025 are
The readings shared in Bluesky on 2 September 2025 are
The readings shared in Bluesky on 1 September 2025 are
The readings shared in Bluesky on 31 August 2025 are
The readings shared in Bluesky on 30 August 2025 are
The readings shared in Bluesky on 29 August 2025 are
The readings shared in Bluesky on 28 August 2025 are
The readings shared in Bluesky on 27 August 2025 are
The readings shared in Bluesky on 26 August 2025 are
The readings shared in Bluesky on 25 August 2025 are
The readings shared in Bluesky on 24 August 2025 are
The readings shared in Bluesky on 23 August 2025 are
The readings shared in Bluesky on 22 August 2025 are
The readings shared in Bluesky on 20 August 2025 are
The readings shared in Bluesky on 19 August 2025 are
The readings shared in Bluesky on 18 August 2025 are
The readings shared in Bluesky on 17 August 2025 are
The readings shared in Bluesky on 16 August 2025 are
The readings shared in Bluesky on 15 August 2025 are