Problema de Erdős #728, resuelto por IA de forma casi autónoma

 (mathstodon.xyz)
2 puntos por GN⁺ 2026-01-10 | 1 comentarios | Compartir por WhatsApp
  • El problema de Erdős #728 fue resuelto recientemente de forma casi autónoma por herramientas de IA, marcando un nuevo hito en la automatización de la investigación matemática
  • El problema era originalmente una pregunta sobre la factorización prima de coeficientes binomiales planteada en 1975 por Erdős, Graham, Ruzsa y Strauss, y durante mucho tiempo no pudo abordarse con claridad debido a condiciones ambiguas
  • ChatGPT generó una prueba bajo restricciones ajustadas, y Aristotle la formalizó como una prueba formal en Lean, corrigiendo errores automáticamente
  • Después, varios participantes la reescribieron en lenguaje natural con ChatGPT y mejoraron iterativamente una versión con mejores conexiones con la literatura y una estructura narrativa más sólida
  • Terence Tao evaluó que este proceso muestra el potencial de la rápida capacidad de la IA para redactar y corregir pruebas para cambiar la forma misma en que se escriben los artículos de investigación

El problema de Erdős #728 resuelto por IA

  • La aplicación reciente de herramientas de IA a la resolución de problemas de Erdős mostró un nuevo avance, y el problema #728 fue resuelto por IA de forma casi autónoma
    • Tras intentos iniciales, se logró el éxito en una versión corregida que incorporó retroalimentación
    • El resultado no pudo reproducirse de forma idéntica en la literatura existente, aunque sí había resultados parecidos con métodos similares
  • Este caso muestra que en los últimos meses la capacidad de la IA para resolver problemas matemáticos realmente ha mejorado
    • En el pasado también hubo casos en los que la IA resolvió problemas de Erdős, pero la mayoría después resultó corresponder a soluciones que ya existían en la literatura
  • En este caso, el enunciado original de Erdős había sido presentado de forma incorrecta y solo recientemente fue reconstruido en la forma pretendida
    • Esto explicaría por qué había poca investigación relacionada en la literatura previa

Historia del problema y enfoque inicial

  • En 1975, Erdős, Graham, Ruzsa y Strauss estudiaron la factorización prima del coeficiente binomial (2n choose n) y plantearon varios problemas relacionados
    • Uno de ellos preguntaba si existen infinitos valores de a, b y n que satisfagan la condición a!b! | n!(a+b−n)! y a+b > n + C log n
    • Sin embargo, varias partes estaban descritas de forma ambigua, incluido el tamaño de C (si era pequeño o grande)
  • Hace unos meses, el equipo de AlphaProof encontró una solución simple al problema, pero no coincidía con el espíritu del problema previsto, por lo que se añadió la restricción a,b ≤ (1−ε)n
    • Incluso después, una búsqueda bibliográfica asistida por IA apenas encontró trabajos relacionados

Colaboración entre ChatGPT y Aristotle

  • El 4 de enero, ChatGPT generó una prueba para el caso de C pequeño bajo las restricciones ajustadas
    • Esa prueba fue formalizada por Aristotle como una prueba formal en Lean
    • Más tarde, al revisar el texto original, se confirmó que el artículo original ya trataba el caso de C pequeño
  • Otro participante convirtió la prueba en Lean a lenguaje natural con ChatGPT y, mediante conversaciones adicionales, redactó una versión mejorada
    • Esa versión llenó algunos huecos de la demostración, pero aún conservaba un estilo torpe característico de la IA y falta de citas bibliográficas
    • Aun así, alcanzó un nivel lo bastante legible como para comprender la idea central

Reescritura a gran escala y resultado mejorado

  • Con prompts adicionales, ChatGPT generó una prueba ampliada al caso de C grande
    • Hubo algunos errores, pero Aristotle los corrigió automáticamente y completó una prueba verificada en Lean
  • Después de que un tercer participante comprimiera la prueba en Lean, otro participante, mediante una larga conversación con ChatGPT, la reescribió en una forma más acabada
    • Fortaleciendo las conexiones con la literatura y la estructura narrativa en formato de artículo
    • El resultado fue evaluado como de menor apariencia de texto generado por IA y con una calidad cercana a la de un artículo de investigación
    • Tao mencionó que revisó este texto en el foro de problemas de Erdős

Cómo la IA está cambiando la forma de escribir artículos de investigación

  • Tao considera que en el artículo final las partes clave todavía deben ser escritas por humanos, pero
    • evalúa que la combinación de IA y Lean elevó de forma drástica la velocidad de redacción y corrección de pruebas
  • Antes, hacer que un artículo resultara agradable de leer requería mucho tiempo, y
    • incluso las revisiones en respuesta a comentarios de revisión solían limitarse a cambios locales
  • Pero ahora, la combinación de la capacidad de la IA para generar y corregir texto y la verificación de las herramientas de prueba formal permite
    • generar rápidamente nuevas versiones de un artículo con distintos niveles de precisión y narración
  • Además de un único “artículo oficial”, podrían existir múltiples versiones auxiliares generadas por IA,
    • lo que abre la posibilidad de aportar diversas perspectivas y valor adicional

Reacción de la comunidad

  • Algunos usuarios describieron el valor adicional de los documentos generados por IA como la capacidad de ver las cosas desde otros ángulos
  • Otros matemáticos plantearon la necesidad de medir la originalidad de los resultados de IA o evaluar su similitud con la literatura existente
    • Por ejemplo, se propuso una medición cuantitativa de similitud mediante la comparación de la longitud de pruebas formales en Lean
  • Otro comentario señaló que, así como en el refactoring de código, la IA puede reescribir un artículo de forma global,
    • por lo que los investigadores deberían concentrarse más en diseñar la estructura documental de más alto nivel
  • Algunos mostraron escepticismo ante la posibilidad de que la IA sustituya el papel del matemático, pero
    • otros lo valoraron como una nueva oportunidad para la colaboración y la expansión del pensamiento

Lecturas relacionadas

1 comentarios

 
GN⁺ 2026-01-10
Opiniones de Hacker News

  • Trabajo en Harmonic y quiero aclarar algunos malentendidos sobre Aristotle que hemos visto
    Aristotle aprovecha activamente las técnicas más recientes de IA, incluyendo modelado del lenguaje
    Si ingresas una demostración informal en inglés, hay una alta probabilidad de que se traduzca a Lean si la demostración es correcta. Es decir, eso se vuelve una señal fuerte de que la demostración en inglés está bien fundamentada
    Una vez que queda formalizada en Lean, ya no hay dudas de que la demostración es correcta. Ese es nuestro enfoque central: si encontramos una respuesta mediante exploración impulsada por IA, podemos garantizar la exactitud del resultado sin importar su complejidad

    • Me pregunto cómo verifican que la demostración traducida por la IA a Lean realmente sea la formalización correcta del problema. En otros campos, la IA generativa suele producir mentiras plausibles, así que quisiera saber si aquí también podría pasar
    • Me pregunto si hay intentos de aplicar esta tecnología a la verificación de software
      Rust usa un conjunto fijo de reglas para garantizar seguridad de memoria, pero esas reglas son simples y limitadas. Si un sistema como Aristotle pudiera integrarse al compilador y permitir que el código pase automáticamente cuando sea posible demostrar su corrección, sería realmente genial
    • Cada vez que sale un nuevo LLM me cuesta saber si es progreso real o simple benchmark hacking, pero creo que la formalización de demostraciones matemáticas sí muestra avance real
      Me pregunto cuánto falta para que Harmonic pueda formalizar la mayor parte de las matemáticas escritas por humanos. Un competidor, Christian Szegedy, decía que sería posible dentro de este año
    • Dijeron que, si la demostración en inglés es correcta, hay una alta probabilidad de traducirla a Lean, pero me pregunto si eso varía según la dificultad por área dentro de las matemáticas. Tengo entendido que todavía hay muchas áreas de investigación que incluso a los humanos les cuesta formalizar
    • La condición de “si la proposición fue formalizada correctamente” suena como una suposición bastante grande. Como vimos en el reciente caso Navier-Stokes, la formalización en sí no es fácil

  • Por la explicación de Terence Tao, parece que un humano fue pasando resultados entre dos herramientas de IA, y que la IA cumplió el rol de rellenar los huecos que el humano había encontrado
    Se parece más a una colaboración entre humanos e IA que a una resolución completamente autónoma. O sea, expertos guiando y la IA asistiendo

    • Sí, yo también entiendo que fue una interacción entre Aristotle, ChatGPT y un usuario excepcionalmente capaz
    • Según entendí, no fue Tao ni la comunidad quienes encontraron directamente los huecos, sino que usaron un verificador automático de demostraciones. Más bien parece algo como 90% IA / 10% humano
    • Hay una explicación detallada del autor en Reddit — publicación de Reddit
    • Para entender el nivel de experiencia y esfuerzo humano involucrado, recomiendo leer el hilo del foro de problemas de Erdős
    • Como dato, este sitio fue creado por el matemático Thomas Bloom, y ChatGPT ayudó con la configuración técnica (cita del FAQ)

  • Reconstituir demostraciones existentes o combinarlas de nuevas maneras es un proceso tedioso o complejo para los humanos, pero la IA puede hacerlo a velocidad sobrehumana
    Este enfoque podría abrir posibilidades enormes incluso antes de llegar a AGI. Parece posible que llegue una era en la que los matemáticos usen IA como herramienta para abordar problemas difíciles como los Millennium Prize Problems

    • No creo que haya una frontera clara entre reconstruir demostraciones existentes y crear matemáticas completamente nuevas
    • Como las matemáticas son lógicas, supongo que ya deben existir muchos algoritmos para este tipo de exploración, pero no parece ser solo un simple problema de búsqueda
    • Yo también estoy de acuerdo con la parte de reconstruir demostraciones existentes. Verificar lo que produce un LLM sigue siendo una tarea tediosa, pero aun así me parece mejor que hacerlo completamente a mano
      El valor real de los LLM está en proponer nuevas perspectivas en temas que pueden expresarse con lenguaje
    • A este fenómeno yo le llamo “refactorización científica”. Por ejemplo, cambiar una constante y volver a desarrollar la lógica; la IA ahora puede hacer ese tipo de experimentos automáticamente
    • Si una IA capaz de demostrar teoremas complejos no es AGI, entonces me pregunto qué sí lo sería

  • En la explicación escrita por la persona que realmente resolvió el problema, impresiona que el resultado se obtuvo sin un pipeline enorme y con solo unos pocos prompts
    Los modelos recientes usan muchos más recursos de cómputo, así que esto más bien parece un resultado de línea base

  • Terence Tao creó una página wiki llamada “AI contributions to Erdős problems”
    Según la página de GitHub y esta publicación en Mathstodon, este resultado (problema 728) es el primer ‘ítem verde’ de esa página, es decir, el primer caso realmente resuelto por IA

    • Curiosamente, la mayoría de las demostraciones formalizadas por IA de la sección 6 de la wiki se completaron en los últimos meses. Da ganas de ver lo que viene

  • Me pregunto si especialistas en campos complejos como física o matemáticas también conversan con IA para recibir ayuda

    • Tengo un doctorado posdoctoral en matemáticas puras y ahora trabajo como científico de datos. La IA ayuda mucho con la revisión de literatura o para repasar rápido matemáticas con las que no estás familiarizado
      Viéndolo por áreas, su utilidad baja en este orden: programación > ML aplicado > estadística/matemática aplicada > matemática pura
    • No soy físico, pero gracias a la IA ahora tardo mucho menos en encontrar las fórmulas o papers que necesito. Eso sí, siempre hay que verificar los resultados
    • Desde la perspectiva de alguien que investiga modelos de deep learning y nuevas estructuras de attention, ChatGPT es muy útil para buscar papers y explorar ideas relacionadas
    • Como aficionado a las matemáticas, los LLM me dan feedback sobre mis intentos o me orientan hacia soluciones existentes. Como matemáticas por diversión, es una herramienta bastante entretenida
    • Hago investigación en geometría algebraica y, fuera de la búsqueda de bibliografía, todavía no me ha ayudado mucho. También varía bastante según el modelo

  • Ya puedes probar Aristotle directamente — https://aristotle.harmonic.fun/

    • También me pregunto si están probando la IA con el dataset formal-conjectures de DeepMind
    • En la documentación dice “uvx aristotlelib@latest aristotle”, pero en realidad debería ser “uvx --from aristotlelib@latest aristotle”
      Además, el enlace a la página personal de Stanford está mal (hay que quitar www)
    • Esto es tan interesante que merecería un hilo aparte en HN. Si yo fuera el CEO, incluso publicaría un post de presentación (enlace de referencia)

  • Este resultado es un teorema sobre enteros, un área donde la infraestructura de Mathlib da muy buen soporte
    Las definiciones usadas tampoco son complejas, así que este tipo de demostraciones tiene alta probabilidad de éxito. Aun así, es un logro realmente impresionante

  • Es un caso que muestra el potencial de enfoques de IA especializados más allá de los LLM
    El paper de Aristotle está en arXiv:2510.01346
    Que use arquitectura Transformer no significa automáticamente que sea un LLM — no se le puede llamar LLM si no fue entrenado con datos de lenguaje

    • Parece que la confusión viene de que mucha gente usa “LLM” como si fuera sinónimo de “GenAI”
    • Dijiste “enfoque que no es LLM”, pero ¿no se usó ChatGPT en realidad?
    • Sí, en efecto se usó ChatGPT
    • Según el paper, en las tres etapas intervienen LLM grandes basados en Transformers
      1. cumplen la función de policy/value en Monte Carlo Graph Search
      2. el sistema de razonamiento informal usa chain of thought
      3. AlphaGeometry también usa un modelo de lenguaje neuro-simbólico
        O sea, todas las etapas están basadas en LLM

  • En 2026 parece probable que la IA empiece a abordar cada vez más problemas abiertos de matemáticas
    Este caso tampoco fue completamente autónomo, pero aun así la IA prácticamente lo resolvió sola después de recibir feedback humano
    Creo que ya se acabó la discusión de que “los LLM son solo loros estocásticos”. De ahora en adelante, la discusión real será cómo llevar esto a aplicaciones prácticas

    • En 2026 podría haber un avance explosivo en matemáticas
    • Es probable que este resultado sea un remix de demostraciones similares que estaban en los datos de entrenamiento, pero esa capacidad de remix por sí sola ya es poderosa
    • Sigue haciendo falta verificación independiente. Cuesta confiar solo en afirmaciones de una empresa