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

El artículo What's next for AI and math, publicado ayer, examina la transformación que la inteligencia artificial está generando en el ámbito matemático. La iniciativa expMath (Exponentiating Mathematics) de DARPA busca revolucionar el progreso matemático mediante una IA coautora capaz de abordar problemas de alta complejidad. Aunque los modelos de lenguaje grandes (LLMs) han demostrado un rendimiento excepcional en problemas de nivel escolar y universitario —superando frecuentemente a los humanos en exámenes como la AIME (American Invitational Mathematics Examination)— estos sistemas operan principalmente siguiendo patrones previamente establecidos. No obstante, cuando se enfrentan a desafíos de investigación abiertos y sin precedentes, como los planteados en el nuevo test FrontierMath, las limitaciones actuales de la IA se manifiestan claramente, revelando una brecha considerable entre las capacidades actuales y la resolución de problemas del calibre de la Hipótesis de Riemann.

Pese a estas limitaciones, la IA está realizando contribuciones significativas al asistir a los matemáticos en la exploración de nuevos enfoques y la identificación de rutas prometedoras. Herramientas como AlphaEvolve y PatternBoost han sido específicamente diseñadas para generar hipótesis, evaluar soluciones potenciales y descartar aproximaciones infructuosas, optimizando así el tiempo de investigación. Paralelamente, se están desarrollando metodologías para simplificar las complejas secuencias de pasos requeridas para resolver problemas de extrema dificultad, como se evidenció en el reciente avance relacionado con la conjetura de Andrews-Curtis.

Sin embargo, la intuición profunda y la creatividad conceptual que caracterizan a los grandes descubrimientos matemáticos permanecen como dominios esencialmente humanos. En este contexto, la IA funciona como una herramienta potente que complementa y amplifica la investigación matemática, pero la chispa de genialidad —esa capacidad de "pensar fuera de los marcos establecidos"— continúa siendo patrimonio exclusivo de la mente humana.

The readings shared in Bluesky on 5 June 2025 are

• Exceptional set in the abc conjecture (in Lean). ~ Jared Duker Lichtman, Bhavik Mehta. #ITP #LeanProver #Math
• IDE for validating specifications. ~ Evan Miyazono, Daniel Windham, Alexandre Rademaker. #ITP #LeanProver
• Faithful logic embeddings in HOL — Deep and shallow (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• A verified reduction algorithm from MLSSmf to MLSS. ~ Yiran Duan, Lukas Stevens. #ITP #IsabelleHOL #Math
• David Poole on knowledge graphs and relational learning. #AI #LogicProgramming
• IA y matemáticas (presente y futuro). #IA #Matemáticas

The readings shared in Bluesky on 4 June 2025 are

• Mathematics in Lean (Release v4.19.0). ~ Jeremy Avigad, Patrick Massot. #ITP #LeanProver #Math
• Functional programming in Lean. ~ David Thrane Christiansen. #ITP #LeanProver #FunctionalProgramming
• The concept of definition: in mathematics, and in computational logic. ~ Lawrence Paulson. #Logic #Math #ITP