Ayer, en su conferencia "AI for Math: The future of collaborative discovery", Mateja Jamnik presentó una visión de la inteligencia artificial no como una simple herramienta para resolver problemas, sino como un socio colaborativo en el descubrimiento matemático. Su trabajo explora cómo las máquinas pueden proponer ideas y acelerar la investigación. A través de un estudio empírico con matemáticos, demostró que la interacción humano-IA es compleja; una respuesta de la IA no necesita ser perfectamente correcta para ser útil, ya que incluso ideas parcialmente erróneas pueden inspirar nuevas vías de pensamiento, mientras que respuestas correctas pero verbosas pueden resultar inútiles.

El núcleo técnico de su propuesta, materializado en trabajos como su artículo "Draft, sketch, and prove: Guiding formal theorem provers with informal proofs", es un ciclo auto-mejorable que integra el vasto conocimiento matemático informal. A través de la arquitectura ‘Borrador, Esquema y Prueba’ descrita en dicho artículo, la IA traduce pruebas humanas a un formato formal y riguroso. Este ciclo culmina en un sistema ‘conjeturador-demostrador’ que genera progresivamente nuevas conjeturas, las evalúa según su capacidad para ayudar a resolver problemas más difíciles y utiliza las mejores para mejorar continuamente, acercándose así a la resolución de teoremas que antes eran inaccesibles.

El objetivo final es integrar plenamente al ser humano en este ciclo de descubrimiento. Jamnik imagina un futuro donde los matemáticos interactúen con este sistema para proponer y evaluar conjeturas, guiando la dirección de la investigación. Su conclusión es que la IA no reemplazará a los matemáticos, sino que los potenciará, creando una sinergia entre la intuición humana y la capacidad de la máquina. El futuro de las matemáticas, según su visión, es una era de descubrimiento colaborativo entre humanos y máquinas.

En su conferencia de ayer "AlphaProof: When RL meets formal maths", Thomas Hubert de Google DeepMind presentó AlphaProof, un sistema de inteligencia artificial que aplica los principios del aprendizaje por refuerzo (RL, del inglés "Reinforcement learning") al dominio de las matemáticas formales. El concepto fundamental radica en que los asistentes de demostración como Lean proporcionan el entorno perfecto para el RL: un espacio de experimentación masiva con retroalimentación inequívoca (una prueba matemática es correcta o incorrecta, sin ambigüedades). Siguiendo el paradigma exitoso de sistemas como AlphaGo Zero, AlphaProof está diseñado para generar conocimiento matemático de forma autónoma, trascendiendo la mera imitación de demostraciones humanas preexistentes.

La arquitectura de AlphaProof se estructura en un proceso de múltiples fases que combina diferentes técnicas de aprendizaje automático. Inicialmente, emplea modelos de lenguaje para autoformalizar problemas matemáticos expresados en lenguaje natural hacia el código formal de Lean, generando así un extenso conjunto de datos de entrenamiento. Su modelo demostrador experimenta dos etapas: primero, un entrenamiento supervisado utilizando la biblioteca mathlib, seguido de un refinamiento intensivo mediante RL que resuelve millones de problemas matemáticos. Para desafíos particularmente complejos —como los de la Olimpiada Internacional de Matemáticas (IMO)—, el sistema implementa una estrategia de adaptación en tiempo real, generando y resolviendo múltiples variantes de un problema para desarrollar gradualmente la intuición necesaria.

Los resultados validan el potencial transformador de AlphaProof como herramienta matemática colaborativa. El sistema alcanzó una puntuación equivalente a una medalla de plata en la IMO y, durante una demostración en vivo durante la conferencia, asistió exitosamente a un matemático a completar los pasos de una prueba compleja relacionada con la función zeta de Riemann. Hubert enfatiza que el objetivo trasciende las competiciones académicas: la meta fundamental es contribuir significativamente a la investigación matemática contemporánea, convirtiendo AlphaProof en una útil para la comunidad matemática que facilite el descubrimiento y verificación de nuevas verdades matemáticas.

The readings shared in Bluesky on 9 June 2025 are

• Formalizing invisible mathematics: case studies from higher category theory. ~ Emily Riehl. #ITP #LeanProver #Math #CategoryTheory
• Sequencelib: A platform for formalizing in Lean 4 sequences from "The On-Line Encyclopedia of Integer Sequences" (OEIS). ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
• At secret math meeting, researchers struggle to outsmart AI. ~ Lyndie Chiou. #AIforMath #AI #LLMs #Math
• Comparing code: Spatial reasoning with zigzag patterns! ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Exploring topological spaces with Prolog: A practical approach using "Mathematics with Prolog". ~ Kenichi Sasagawa. #Prolog #LogicProgramming #Math
• Teaching and learning mathematics with Prolog. ~ Tom Bensky (2021). #Prolog #LogicProgramming #Math
• Evaluando la IA con problemas matemáticos inéditos de nivel experto. #AIforMath #AI #LLMs #Math
• Curso "Lógica informática (2012-13)". #Lógica #ProgramaciónLógica #Prolog
• Curso "Lógica matemática y fundamentos (2012-13)". #Lógica #Haskell #ProgramaciónFuncional #Isabelle/HOL

El artículo Inside the secret meeting where mathematicians struggled to outsmart AI documenta una reunión extraordinaria celebrada en Berkeley a mediados de mayo de 2025, donde treinta de los matemáticos más prestigiosos del mundo se enfrentaron en un duelo intelectual contra o4-mini, el avanzado modelo de razonamiento de OpenAI, en un desafío organizado por Epoch AI bajo el nombre FrontierMath. La misión parecía clara: crear problemas de investigación de nivel de doctorado que los humanos pudieran resolver pero que resultaran infranqueables para la inteligencia artificial. Sin embargo, los participantes experimentaron una sorpresa mayúscula al descubrir que el sistema resolvía algunos de los problemas más complejos que le presentaron, exhibiendo una capacidad de razonamiento que trascendió todas sus expectativas.

La extraordinaria destreza del sistema quedó vívidamente ilustrada en la experiencia del matemático Ken Ono, quien presenció cómo o4-mini resolvía un problema abierto de nivel de doctorado en apenas diez minutos: primero exploró sistemáticamente la literatura especializada, después resolvió una versión simplificada como ejercicio de "aprendizaje", y finalmente presentó una solución rigurosa al desafío principal. Este enfoque metodológico, que Ono caracterizó como propio del razonamiento científico auténtico, no fue un caso aislado, ya que el grupo logró formular únicamente diez problemas que resistieron los embates de la IA, subrayando la eficacia abrumadora del sistema.

El encuentro concluyó con una profunda reflexión sobre las transformaciones que se avecinan en el campo matemático. Entre las preocupaciones emergentes destacó el fenómeno de la "prueba por intimidación": la tendencia a aceptar los resultados de la IA sin el escrutinio riguroso tradicional. La conclusión consensuada apunta hacia una metamorfosis radical en el rol del matemático profesional, que evolucionará desde el tradicional "solucionador de problemas" hacia una nueva función como "formulador de preguntas estratégicas" que colabora y orienta el potencial de la inteligencia artificial. Como advirtió Ono, subestimar estas herramientas constituye un grave error, dado que ya están superando el rendimiento de los estudiantes de posgrado más talentosos del mundo.

The readings shared in Bluesky on 8 June 2025 are

• The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. ~ Parshin Shojaee et als. #LLMs #Reasoning
• Más allá de la "ilusión de pensar". #LLMs #Reasoning #Math #ITP #LeanProver
• AutoGPS: Un sistema neuro-simbólico para la geometría. #AI #Math
• Curso "Informática (2012-13)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima

El artículo AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning presenta AutoGPS, un sistema paradigmático para la geometría. Este trabajo aborda la dicotomía fundamental entre los modelos neuronales, que destacan en la interpretación multimodal pero carecen de fiabilidad lógica, y los métodos simbólicos, que garantizan el rigor pero son ineficaces para formalizar problemas a partir de entradas complejas. AutoGPS resuelve este dilema mediante un marco neuro-simbólico: un formalizador de problemas multimodales (MPF) traduce la entrada visual y textual a un lenguaje lógico, sobre el cual opera un razonador simbólico deductivo (DSR) para derivar la solución.

La innovación crucial reside en la interacción bidireccional entre ambos componentes. El DSR no se limita a resolver el problema formalizado, sino que actúa como un verificador, validando la interpretación del MPF y pudiendo solicitarle correcciones. Este bucle de retroalimentación garantiza la consistencia lógica de todo el proceso, fusionando la capacidad heurística del modelo neuronal con el rigor inflexible del razonamiento deductivo.

Como resultado, AutoGPS establece un nuevo estado del arte en los benchmarks de referencia, produciendo derivaciones que no solo son correctas, sino también concisas y legibles para un humano. De este modo, redefine el estándar de fiabilidad e interpretabilidad en la resolución automática de problemas matemáticos. La página del proyecto ofrece ejemplos ilustrativos de su funcionamiento.

Un reciente artículo de investigadores de Apple, titulado "The illusion of thinking: A survey of the state of the art in Large Language Models", postula que las impresionantes capacidades de los Grandes Modelos de Lenguaje (LLMs) no derivan de una comprensión o razonamiento genuino, sino de una sofisticada imitación de patrones estadísticos extraídos de vastos corpus de datos. Esta "ilusión de pensar" se vuelve particularmente manifiesta en dominios que exigen una lógica estricta y verificable, como las matemáticas formales. En este campo, la propensión de los LLMs a la "alucinación" y su inherente falta de un modelo causal del mundo limitan fundamentalmente su fiabilidad, incapacitándolos para producir razonamientos complejos de manera autónoma y garantizada.

Para abordar esta limitación estructural, la investigación contemporánea ha centrado sus esfuerzos en el desarrollo de arquitecturas híbridas neuro-simbólicas. Dichos sistemas implementan una división funcional del trabajo computacional: el componente neuronal (el LLM) opera como interfaz de alto nivel, encargado de procesar entradas en lenguaje natural y generar estrategias heurísticas preliminares. Estas propuestas son luego transferidas a un módulo simbólico —ya sea un sistema de cálculo algebraico exacto o un demostrador de teoremas— que actúa como verificador formal. Este último componente, regido por reglas lógicas inflexibles, examina cada inferencia producida por el LLM, proporcionando retroalimentación inmediata y garantizando la corrección deductiva del proceso.

La eficacia de este paradigma ha sido demostrada empíricamente por sistemas de última generación diseñados para resolver problemas de la Olimpiada Internacional de Matemáticas (IMO). Tal como se documenta en el estudio AI achieves silver-medal standard solving International Mathematical Olympiad problems, estas plataformas combinan un LLM encargado de la generación inicial de hipótesis con herramientas especializadas como AlphaProof, un sistema optimizado para demostrar enunciados matemáticos en el lenguaje formal de Lean. Cabe destacar que Lean, lejos de ser una mera herramienta auxiliar, constituye un componente estructural en estos sistemas: su integración permite traducir la capacidad heurística de los LLMs a un marco verificable formalmente. Esta sinergia entre la creatividad inductiva de los modelos neuronales y el rigor de los sistemas simbólicos representa el estado del arte en la construcción de inteligencias artificiales capaces de razonamiento matemático formalmente validable.

The readings shared in Bluesky on 7 June 2025 are

• The bizarre story of a maths proof that is only true in Japan. ~ Jacob Aron. #Math
• La disputa sobre la conjetura abc y el papel de la verificación formal. #Matemáticas #ITP #LeanProver

Leibniz soñaba con un sistema de razonamiento formal, su "Calculemus", que permitiría resolver disputas simplemente diciendo "calculemos". Hoy, esta idea cobra especial relevancia en el centro de una de las controversias más extrañas de las matemáticas modernas, la detallada en el artículo de New Scientist "The bizarre story of a maths-proof that is only true in Japan". El artículo describe cómo la prueba de la conjetura abc del matemático Shinichi Mochizuki, basada en su compleja teoría de Teichmüller Interuniversal (IUT), ha dividido a la comunidad. A pesar de haber sido publicada formalmente en Japón, la mayoría de los matemáticos internacionales la rechazan, siguiendo la crítica de expertos como Peter Scholze que señalan un supuesto "error fatal", creando una división geográfica sin precedentes sobre la validez de un resultado matemático.

La razón de este intenso escrutinio reside en el inmenso poder de la propia conjetura abc. Esta establece una conexión profunda entre la suma y la multiplicación de números enteros, postulando que para tres números coprimos a + b = c, el valor de c es casi siempre más pequeño que el "radical" del producto a*b*c (el producto de sus factores primos únicos). Si se demostrara, la conjetura actuaría como una "piedra Rosetta" para la teoría de números, resolviendo de un plumazo una multitud de otros problemas famosos, como el último teorema de Fermat, lo que justifica la frustración y el interés global por resolver esta disputa de una vez por todas.

Para resolver el impasse y cumplir el sueño de Leibniz, la solución definitiva sería utilizar un asistente de pruebas formal como Lean, un software que puede verificar la lógica de una demostración con certeza absoluta, eliminando la ambigüedad humana. Sin embargo, formalizar la novedosa y compleja IUT de Mochizuki es una tarea monumental, considerada casi imposible hoy en día. A pesar de ello, la comunidad de Lean está dando pasos cruciales. Proyectos como Exceptional set in the abc conjecture de Jared Duker Lichtman y Bhavik Mehta no verifican la prueba directamente, pero sí formalizan el enunciado del problema y desarrollan las herramientas y la experiencia necesarias. Estos esfuerzos sientan las bases para que, quizás algún día, esta extraordinaria disputa matemática pueda finalmente ser resuelta mediante el cálculo.

The readings shared in Bluesky on 6 June 2025 are

• Big steps in higher-order mathematical operational semantics. ~ Sergey Goncharov, Pouya Partow, Stelios Tsampas. #Haskell #FunctionalProgramming
• Libro "Matemáticas en Lean4" (versión del 6-junio-25). #ITP #Lean4 #Math