El artículo "LeanTutor: A formally-verified AI tutor for mathematical proofs" aborda un problema común en la educación matemática: los estudiantes tienen dificultades para aprender demostraciones. Actualmente existen dos tipos de herramientas, pero ninguna funciona bien para enseñar. Los chatbots como ChatGPT son fáciles de usar pero dan respuestas directas o incorrectas, sin ayudar realmente al aprendizaje. Los asistentes de demostración como Lean verifican las matemáticas perfectamente, pero son demasiado complicados para principiantes. Se necesita una herramienta que combine lo mejor de ambos: la facilidad del lenguaje natural y la precisión de la verificación formal.

Los autores crearon LeanTutor, un sistema que funciona como tutor inteligente combinando lenguaje natural con verificación formal. El sistema tiene tres partes que trabajan juntas. Primero, el 'autoformalizador' toma lo que escribe el estudiante en lenguaje normal y lo convierte a código Lean para verificar si es correcto. Si hay un error, el 'generador del siguiente paso' calcula cuál sería la respuesta correcta. Finalmente, el 'generador de retroalimentación' convierte esta información técnica en consejos útiles para el estudiante, dándole pistas sin revelar directamente la solución.

Los investigadores probaron LeanTutor usando un nuevo conjunto de datos llamado PeanoBench y los resultados fueron positivos. El sistema logró convertir correctamente la mayoría de los pasos que escribían los estudiantes y detectó muchos errores. Cuando compararon la retroalimentación de LeanTutor con otros sistemas, encontraron que era más precisa y útil para los estudiantes. Los autores concluyen que este enfoque de combinar IA conversacional con verificación formal es una buena dirección para crear mejores herramientas educativas.

Este trabajo presenta una idea muy buena para mejorar la educación matemática. La principal fortaleza es que logra combinar de manera inteligente la facilidad de uso del lenguaje natural con la precisión matemática de Lean. Sin embargo, también tiene algunas limitaciones importantes. El sistema necesita tener de antemano la solución correcta del problema, y asume que los pasos del estudiante se pueden traducir directamente a código Lean, lo que podría no funcionar en situaciones más complejas. A pesar de estas limitaciones, LeanTutor es un buen primer paso que muestra cómo la IA puede ayudar a enseñar matemáticas de forma más efectiva y segura.

En su conferencia "Will computers prove theorems?", Kevin Buzzard plantea que los ordenadores ya demuestran teoremas, pero la pregunta crucial es cómo pueden transformar la investigación matemática. Aunque reconoce la utilidad de las herramientas actuales como las redes neuronales para identificar patrones, su aplicación permanece limitada. Los modelos de lenguaje como ChatGPT, por su parte, pueden ofrecer ideas valiosas, pero fracasan rotundamente en el razonamiento lógico: tienden a "alucinar" o inventar detalles para parecer convincentes, lo que los convierte en herramientas poco confiables para las matemáticas rigurosas.

La solución que propone Buzzard para superar estas limitaciones radica en la sinergia entre la inteligencia artificial y los asistentes de demostración formal como Lean. Su propuesta consiste en entrenar modelos de IA para que generen pruebas directamente en código de Lean, en lugar de utilizar lenguaje natural. De este modo, el asistente de demostración funciona como un verificador infalible: cualquier argumento lógicamente incorrecto será rechazado automáticamente por el sistema. Esta metodología obligaría a la IA a evolucionar desde la mera imitación de patrones hacia la construcción de razonamientos lógicamente verificables.

No obstante, el principal obstáculo para materializar esta visión es la escasez de matemáticas modernas y avanzadas formalizadas en Lean, elementos esenciales para el entrenamiento de estos modelos. Buzzard concluye con un llamamiento directo a la comunidad matemática: considera que es responsabilidad de los investigadores emprender la tarea fundamental de formalizar el conocimiento de sus respectivos campos, tal como él mismo está haciendo con el último teorema de Fermat. Argumenta que este esfuerzo resulta crucial para desarrollar las herramientas que revolucionarán la disciplina, a pesar de que el sistema académico actual no reconozca ni recompense adecuadamente este tipo de contribuciones.

The readings shared in Bluesky on 10 June 2025 are

• Inductive definitions. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• The equational theories project: advancing collaborative mathematical research at scale. ~ Terence Tao et als. #ITP #LeanProver #Math #AIforMath
• New AI stuns mathematicians with its problem-solving skill. ~ David H Bailey. #AI #LLMs #Math #AIforMath #ITP #LeanProver
• Premise selection for a Lean hammer. ~ Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck. #ITP #LeanProver #AI
• Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. ~ Chengwu Liu et als. #LLMs #Math #ITP #LeanProver
• AlphaProof: When RL meets formal maths. ~ Thomas Hubert. #AI #Math #AIforMath #ITP #LeanProver #AlphaProof
• AI for Math: The future of collaborative discovery. ~ Mateja Jamnik. #AIforMath
• Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. #LLMs #Math #ATP #Prover9
• Dr. Neckbeard, or how I learned to stop worrying and love Emacs. ~ Watts Martin. #Emacs
• Revistas, editoriales y congresos depredadores. #Investigación
• AlphaProof: Aprendizaje por refuerzo aplicado a la demostración matemática. #AI #Math #AIforMath #ITP #LeanProver #AlphaProof
• El futuro de las matemáticas: Descubrimiento colaborativo entre humanos y máquinas. #AIforMath #AI #Math
• El proyecto ETP (Un caso de estudio en investigación matemática colaborativa y formalizada). #AIforMath #ITP #LeanProver #Math

Hoy, en su conferencia "The equational theories project", Terence Tao defendió que la investigación matemática debe evolucionar hacia un modelo colaborativo a gran escala, semejante al empleado en otras disciplinas científicas. Esta transformación requiere el uso de herramientas modernas como plataformas colaborativas (GitHub), asistentes de prueba formales (Lean) y automatización mediante inteligencia artificial. El proyecto ETP (Equational Theories Project) constituye un ejemplo paradigmático de esta nueva aproximación a la investigación matemática.

El proyecto nació de una pregunta aparentemente simple planteada en el foro MathOverflow, pero pronto adquirió una dimensión extraordinaria: mapear completamente el "gráfico de implicaciones" entre 4,692 leyes algebraicas únicas dentro de estructuras elementales denominadas magmas. Esta ambiciosa meta implicaba resolver más de 22 millones de problemas individuales, donde cada par de leyes requería encontrar una prueba de implicación o desarrollar un contraejemplo que la refutara. La magnitud descomunal de este desafío lo convertía en una tarea imposible de abordar mediante los métodos tradicionales de investigación individual o de pequeños equipos.

La estrategia implementada por el ETP consistió en un flujo de trabajo híbrido y descentralizado de notable innovación. La componente humana aprovechó la creatividad de una extensa comunidad de colaboradores para desarrollar pruebas y contraejemplos ingeniosos, mientras que la componente computacional empleó masivamente probadores automáticos de teoremas (ATPs) y otras herramientas para resolver millones de casos más directos. El elemento fundamental que garantizó la integridad del proyecto fue la formalización exhaustiva de cada resultado en el asistente de pruebas Lean, asegurando una corrección absoluta y creando una base de conocimiento completamente verificada y confiable.

En el plazo extraordinariamente breve de tres meses, el proyecto logró resolver prácticamente la totalidad de los 22 millones de problemas planteados. Además, el proceso de abordar los casos más complejos estimuló el desarrollo de técnicas matemáticas innovadoras, culminando con la formulación de un nuevo y fascinante problema abierto. El ETP demostró que este modelo colaborativo trasciende la mera verificación de conocimiento existente para convertirse en un motor poderoso de descubrimiento matemático, estableciendo así un precedente exitoso para una investigación matemática más abierta, transparente y asistida computacionalmente.

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.