Matemáticos humanos, superados por la IA en la búsqueda de contraejemplos

• Modelos de las familias ChatGPT y Claude crearon en apenas unas semanas contraejemplos a la conjetura de distancia unitaria de Erdős, a una pregunta de Grothendieck sobre esquemas de grupos y a la Jacobian Conjecture; algunos fueron verificados en Lean
• Sol, de OpenAI, formalizó en 3 semanas el contraejemplo de Erdős y los resultados necesarios de teoría global de cuerpos de clases en 1,2 millones de líneas de código Lean, una escala que supera la mitad de los 2,3 millones de líneas de mathlib escritas durante 9 años
• Para la pregunta de Grothendieck, de 60 años de antigüedad, Sol encontró un contraejemplo de 12 páginas y Fable lo formalizó en 1.076 líneas en 4 horas, confirmando la existencia de un esquema de grupos de orden 4 que no es aniquilado por 4
• La formalización automática también aceleró mucho la investigación: Andrew Yang escribió unas 250.000 líneas de código Lean en aproximadamente 2 semanas y prácticamente completó el proyecto de formalizar el teorema de levantamiento de modularidad necesario para el último teorema de Fermat
• No se puede confiar sin más en la matemática informal generada por IA, pero si una conjetura se convierte en una proposición precisa de Lean, las pruebas y refutaciones pueden verificarse mecánicamente; los humanos deben extraer de los contraejemplos una comprensión matemática más profunda

---

La conjetura de distancia unitaria de Erdős y la teoría global de cuerpos de clases

• El 20 de mayo de 2026, ChatGPT refutó la conjetura de distancia unitaria de Erdős en geometría discreta
  • Construyó un contraejemplo usando un profundo teorema de teoría de números de Golod y Shafarevich de la década de 1960
  • Varios matemáticos revisaron el argumento de antemano y lo consideraron válido, pero al momento de publicarse no había una formalización en Lean
• El 26 de mayo, Mike Freedman, ganador de la Medalla Fields y director científico de Logical Intelligence, informó que su sistema había formalizado automáticamente en Lean todo el artículo de ChatGPT
  • El alcance formalizado era la proposición de que el teorema de Golod–Shafarevich implica el contraejemplo de Erdős
  • El teorema de teoría de números subyacente requiere por sí solo más de 100 páginas y depende de una gran parte de la teoría global de cuerpos de clases
• Después de la escuela de verano de formalización de la teoría de cuerpos de clases de 2025, durante un año los casos locales quedaron casi completos, pero el caso global seguía sin resolverse

La formalización completa de 1,2 millones de líneas creada por Sol

• El 26 de junio, Boris Alexeev, de OpenAI, anunció en Lean Zulip que había guiado al nuevo modelo Sol para crear una formalización completa del contraejemplo de Erdős, sin asumir nada salvo los axiomas matemáticos
• Sol generó 1,2 millones de líneas de código Lean durante 3 semanas
  • mathlib, escrita a lo largo de 9 años, tiene 2,3 millones de líneas
  • La calidad del código era irregular, pero efectivamente probaba resultados difíciles de la teoría global de cuerpos de clases y teoremas no triviales sobre cohomología de cuerpos numéricos
• Como Lean es un lenguaje de programación que puede ejecutar comandos arbitrarios, el código generado se ejecutó en un sandbox por la posibilidad de código malicioso
• Esta escala y velocidad llevaron a la conclusión de que el desarrollo matemático a gran escala generado por IA es inevitable

Taller Formalizing Fermat y accesibilidad de herramientas

• Al taller Formalizing Fermat, realizado del 6 al 10 de julio, asistieron 25 personas, pero el sistema de formalización automática del patrocinador Logos Research solo podía ser usado por 5 personas a la vez
• A todos los asistentes se les dio una suscripción de un mes a Claude Max para que pudieran usar Claude Fable, y OpenAI también ofreció gratis acceso de un mes a ChatGPT Pro
  • Sol estaba previsto para lanzarse el 9 de julio
  • Fable estaba previsto para cerrarse el 7 de julio, pero en la práctica el acceso se mantuvo
  • Los asistentes pudieron usar Sol y Fable durante 4 de los 5 días del taller, y las herramientas de Logos durante todo el período
• Para desarrollar la teoría de esquemas de grupos finitos planos necesaria para formalizar el último teorema de Fermat, se ingresaron artículos clásicos en Fable y ChatGPT y se les pidió escribir explicaciones en lenguaje natural
  • Logos detectó que una proposición incluida en la explicación era falsa y produjo un contraejemplo explícito
  • Al verificarlo, se comprobó que el documento generado por LLM que describía una construcción estándar era incorrecto, y que los humanos habían pasado por alto el error durante la lectura
  • La diferencia fue que, en vez de simplemente responder que no entendía el argumento, proporcionó una prueba de que el argumento era incorrecto

La pregunta de Grothendieck sobre esquemas de grupos

• Akhil Mathew, profesor de UChicago, propuso a la IA una vieja pregunta de Grothendieck: si todo esquema de grupos finito libre de orden (n) es aniquilado por (n)
  • Deligne probó el caso conmutativo
  • Grothendieck probó el caso en que el espacio subyacente es reducido
  • Rene Schoof trató más casos, y Emiliano Torti también probó un caso más general en un artículo del año anterior
• El 11 de julio, al día siguiente del taller, Sol encontró un contraejemplo y generó un PDF de 12 páginas
  • Cuando se pidió la formalización completa en Lean en lugar del resultado informal, Fable la formalizó automáticamente en 1.076 líneas en 4 horas
• Primero se inspeccionó que el archivo Lean contuviera solo teoremas, sin comandos como borrado de archivos, y luego se compiló en una laptop
  • Se verificó que la proposición usara solo conceptos de mathlib
  • Se comprobó que la proposición realmente expresara la existencia de un contraejemplo
  • Se verificó que la prueba compilara correctamente
  • Toda la verificación tomó menos de 5 minutos
• La verificación confirmó que existe un esquema de grupos de orden 4 que no es aniquilado por 4
• Akhil Mathew envió este contraejemplo como PR a mathlib
• Mientras que el contraejemplo de Erdős tiene alrededor de 1 millón de líneas, el de Grothendieck tiene unas 1.000 líneas y es mucho más simple, pero aun así se convirtió en un caso en el que una máquina resolvió una pregunta de geometría algebraica de 60 años

Reacciones de expertos y teorema de levantamiento de modularidad

• El 14 de julio, un profesor de Imperial College evaluó que el hecho de que el contraejemplo de Grothendieck se hubiera encontrado tan fácilmente solo demostraba que los humanos no habían pensado lo suficiente en ese problema
• El estudiante de doctorado Andrew Yang usó Sol y Fable mientras formalizaba en Lean el teorema de levantamiento de modularidad, importante para el último teorema de Fermat
  • Escribió 250.000 líneas de código Lean en unas 2 semanas
  • Con eso, prácticamente completó el proyecto
• Otro profesor de Imperial consideraba difícil entender que estudiantes de posgrado pagaran USD 200 al mes por Sol y Fable, pero después de ver este resultado concluyó que, más bien, era irracional que un doctorando no gastara USD 200 al mes en esas herramientas
• Harvard ya ofrecía acceso gratuito a Fable a todos los estudiantes de doctorado, investigadores posdoctorales y profesores

Contraejemplo a la Jacobian Conjecture

• Akhil Mathew y Levent Alpöge discutieron formas de encontrar más contraejemplos en geometría algebraica, y Fable encontró un contraejemplo a la Jacobian Conjecture, un famoso problema que llevaba abierto unos 100 años
• Levent Alpöge publicó en X el resultado, que parecía haberse resuelto durante la final del Mundial 2026
• Cuando Akhil Mathew propuso un nuevo PR a mathlib, Paul Lezeau ya había formalizado manualmente el contraejemplo y enviado un PR al repositorio Formal Conjectures de DeepMind
• mathlib no tiene una lista extensa de conjeturas matemáticas, pero el repositorio Formal Conjectures sí la tiene
• Si los humanos se ponen de acuerdo en una proposición Lean que capture fielmente el significado de la conjetura, verificar si el código generado por IA prueba o refuta esa conjetura se vuelve sencillo

Lo que queda para los humanos tras la verificación formal

• En la Jacobian Conjecture, el siguiente paso para los humanos es entender exactamente qué ocurre en ese contraejemplo
• También en el contraejemplo de Grothendieck está en marcha el trabajo de entenderlo con más profundidad, más allá de enumerar representaciones y cálculos arbitrarios sobre anillos
• El valor de un contraejemplo no se limita a cerrar formalmente el problema: se completa en el proceso de extraer comprensión para que los humanos entiendan mejor la matemática

[GN⁺]

Comentarios de Hacker News

• En el posgrado tuve la oportunidad de contribuir directamente a un problema abierto en el seminario de investigación de mi asesor. Un viernes, el profesor presentó una conjetura elegante y hermosa que esperaba que fuera cierta, pero como a mí me gustan las excepciones extrañas y no tenía muchas herramientas de demostración, me enfoqué en buscar un contraejemplo y lo encontré en una hora
  El profesor no logró demostrarla en todo el fin de semana, y eso mostró que cuando personas con herramientas, expectativas y motivaciones distintas miran el mismo problema, pueden contribuir desde direcciones totalmente diferentes. No me puedo comparar con un gran asesor, pero en ese momento sí tenía una razón para mirar en otra dirección, y eso llevó a mi pequeña contribución a la investigación matemática: un contraejemplo

  • Probablemente por eso las máquinas también son buenas para encontrar contraejemplos. No tienen apego estético a una conjetura ni vergüenza de producir un resultado feo
  • Como matemático, mi sensación es la contraria. Una demostración se puede hacer adaptando un poco una demostración conocida, pero construir un contraejemplo suele requerir entender profundamente la estructura del objeto, y muchas veces eso supera mis capacidades
    Aunque quizá sea porque trabajo sobre todo con objetos abstractos difíciles de entender; con números o polinomios podría ser al revés
  • Los profesores, investigadores y docentes que exponen a los estudiantes problemas aún no resueltos y los invitan a participar deberían ser más valorados. En mi primera clase de ingeniería en la universidad, el instructor les dijo a alumnos de primer año: “Estos son problemas que todavía no hemos resuelto, así que si se les ocurre una idea, avísenme”, y me sentí más bienvenido e incluido en la comunidad que nunca; fue una gran inspiración al inicio de los estudios, que fácilmente podría haber sido aburrido
  • En How to Solve It aparece casi la misma historia
  • Hay una anécdota aún más extrema, pero en la dirección opuesta, sobre Zeeman. Pasó años intentando encontrar una esfera anudada en un espacio de cinco dimensiones, luego se dio cuenta de que era imposible y lo demostró en unas horas
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• Yitang Zhang, famoso por la conjetura de los primos gemelos, estudió la conjetura jacobiana durante 7 años en Purdue bajo la dirección de Tzuong-Tsieng Moh. Se descubrió que el paso clave de su tesis dependía de un corolario erróneo de Moh; Moh se negó a escribirle una carta de recomendación, y Zhang no pudo conseguir un puesto docente o de investigación, así que terminó trabajando varios años en Subway
  Me pregunto cómo habría sido si ChatGPT hubiera existido cuando empezó esa investigación en 1986. Ahora es una historia de éxito conmovedora, pero, como dice el verso “庾信平生最萧瑟，暮年诗赋动江关”, provoca sentimientos complejos

  • Una vez, durante la defensa de un doctorado en matemáticas, un profesor del jurado encontró una falla en la demostración. Cuando el estudiante la entendió y preguntó “¿Y ahora qué hacemos?”, el profesor del jurado solo se encogió de hombros
  • Se puede decir que conmueve porque más tarde triunfó con la conjetura de los primos gemelos, pero ya me cansé de este tipo de historias en la academia. Hay demasiada política y manejo de reputación, y Zhang no debería haber pasado por ese sufrimiento
    Al ampliar mi investigación hacia las matemáticas, me sorprendió ver que una parte considerable de las proposiciones en la literatura son falsas, y que eso se ha propagado ampliamente incluso a la literatura aplicada. Incluso cuando se señala el problema, como en la historia de Zhang, muchas veces responden con defensa y negación. Los LLM son útiles para las demostraciones, pero también se equivocan mucho; se parecen a otra persona más que sugiere direcciones de exploración desde una intuición distinta, así que probablemente en 1986 el resultado habría sido el mismo
  • El verso traducido por ChatGPT significa más o menos: “La vida de Yu Xin fue profundamente desolada, pero sus poemas y prosas de la vejez conmovieron ríos y pasos fronterizos”

• En matemáticas, los contraejemplos son muy importantes para pulir definiciones y afinar demostraciones. Recomiendo el libro de 1976 de Imre Lakatos, Proofs and Refutations, y también hay bastantes libros dedicados solo a contraejemplos en topología, probabilidad, análisis y otras áreas
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Si encuentras un contraejemplo, puedes dejar de perder tiempo intentando demostrar una proposición falsa y pasar a otro problema; así que, al menos en matemáticas, eso permite usar el tiempo de la humanidad de manera más productiva

  • Refutar mediante un contraejemplo es efectivo, pero en última instancia no resulta satisfactorio. Da una respuesta, pero no ayuda a entender por qué las matemáticas funcionan así ni conduce a nuevas preguntas
    Mientras los humanos sigan siendo quienes juzgan qué demostración es elegante y reveladora, seguirá habiendo trabajo para los matemáticos humanos
  • Los contraejemplos también sirven para refinar el enunciado de un teorema. En la investigación en ciencias de la computación teórica es común intentar demostrar un teorema que uno desea que sea cierto, encontrar un contraejemplo, ajustar el enunciado y seguir
    También ayuda que muchos teoremas en ciencias de la computación traten con definiciones inductivas y coinductivas
  • En particular, si el contraejemplo fue verificado formalmente, puede convertir casi de inmediato años de esfuerzo especulativo en una respuesta definitiva
  • Pero, en general, no se puede afirmar sin más que el tiempo se haya usado de forma más productiva. Ya sea demostrando o refutando una proposición, y sea esta verdadera o falsa al final, el proceso puede generar nuevas intuiciones

• Parece que la IA también escribirá la versión matemática de La balada de John Henry. Me pregunto quién será el último campeón humano capaz de producir una demostración “digna de figurar en THE BOOK” que ni siquiera una máquina pueda superar
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Esa es una forma poco saludable de ver las matemáticas como si fueran una competencia, como un aficionado al fútbol. Lo más valioso en matemáticas no son solo las demostraciones hermosas, sino también las definiciones útiles; crear buenas definiciones y buenas conjeturas a partir de ellas sigue siendo un terreno que los LLM todavía no intentan conquistar
  • Aún no es tan dramático, pero es posible que pronto lleguemos a ese punto. No hay base estructural para predecir si la capacidad de la IA mejorará de manera asintótica o se acelerará, y ambas posibilidades siguen abiertas respecto a qué problemas podrían resolverse con métodos nuevos
    No entendemos el interior de la capacidad de la IA ni su curva de crecimiento, y ni siquiera sabemos con precisión si está mostrando deliberadamente un rendimiento menor. Podría ser un fenómeno emergente que se resiste a la medición, o podría volverse tan predecible como un reloj en unos años. Nadie lo sabe, y si alguien lo sabe, no lo dice; y quienes hablan más fuerte tampoco saben nada

• Si eso adelanta de forma importante que un estudiante de posgrado logre resultados significativos, no hay razón para no invertir $2,400 al año por estudiante. Frente al costo total, es casi calderilla

  • Algunos estudiantes de posgrado no se ven a sí mismos como una “máquina que produce resultados significativos”, sino como seres éticos. Todos saben que incluso los LLM útiles son difíciles de justificar por los datos de entrenamiento obtenidos sin permiso y su enorme impacto ambiental
  • La beca de manutención del doctorado de la EPSRC es de alrededor de £20,000, así que esto equivale a cerca del 10% del costo anual. Para cada estudiante es una carga grande

• Ojalá hubiera existido una formalización en Lean generada por LLM cuando estaba en la universidad. Las matemáticas en las diapositivas de clase tenían muchos errores, y algunos profesores, mientras decían “la prueba está en las diapositivas”, se negaban a responder pedidos de aclaración y además eran reacios a reconocer los errores
  La prueba en Lean en sí muchas veces no es adecuada para comprender, pero ojalá a partir de ella se pudieran generar argumentos fáciles de entender para una persona

  • Me cuesta estar de acuerdo con la primera afirmación. La curva de aprendizaje es empinada, pero una formalización en Lean, Agda o Rocq bien hecha es excelente para entender una prueba. Una buena formalización muestra de forma estructural el panorama general y el argumento central, y a diferencia de una prueba en papel permite verificar el detalle de cada paso hasta la profundidad que uno quiera
    El repositorio TypeTopology Agda de Martín Escardó es un buen ejemplo. En cambio, las formalizaciones generadas por LLM hoy pueden ser muy desordenadas, así que aunque certifiquen un teorema y contengan argumentos interesantes, hace falta bastante trabajo para pulirlas de una forma que mejore la comprensión matemática. Hay un tutorial interactivo de Agda en lets-play-agda.quasicoherent.io
  • La formalización también puede usarse en un enfoque leibniziano para cerrar discusiones y eliminar por completo cualquier duda

• Me pregunto si para los matemáticos los contraejemplos son algo como los resultados inesperados en las ciencias físicas, molestos en el momento pero enormemente importantes porque revelan la inexactitud de un modelo, o si son más bien como reportes de bugs en programación: detalles menores y fastidiosos

  • Los contraejemplos aclaran el papel de las condiciones. Si hay un contraejemplo lo más simple y fácil de recordar posible que muestre qué falla cuando se viola cada condición de la prueba, resulta muy útil
    Los matemáticos tienden a llevar un zoológico de contraejemplos en la cabeza. Incluso al reconstruir un teorema, pueden recordar contraejemplos agudos y memorables y estrechar el dominio y las condiciones para excluirlos
  • Hay libros didácticos como Counterexamples in Topology y Counterexamples in Analysis que enseñan las sutilezas de un campo a través de contraejemplos. Son populares porque es más fácil aprender los detalles con ejemplos patológicos o degenerados que estudiando solo los objetos normales previstos

• Buena parte de estas matemáticas es difícil de entender, pero en general parece tratar sobre demostrar teoremas. Si la matemática con IA sigue acelerándose, me pregunto si en el futuro descubrirá incluso nuevas matemáticas que luego se apliquen a la ingeniería o la biomedicina, si estamos justo antes de un gran avance de la humanidad, o si se quedará en demostrar lo ya conocido

  • Es posible. La detección comprimida puede verse como un ejemplo de nuevas matemáticas aplicadas a la biomedicina, y puede reducir mucho el tiempo de las resonancias magnéticas, mejorando la experiencia del paciente y permitiendo que más personas se hagan el estudio
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Aunque llegue a aplicarse en ingeniería y biomedicina, probablemente sea algo de largo plazo, pero el desarrollo de nuevos métodos matemáticos podría volverse importante antes para la investigación en física fundamental. A menudo ha habido grandes mejoras en los modelos cuando aparecieron herramientas matemáticas que permitieron representarlos o verificarlos
  • Incluso si es posible, tardará muchísimo. En la mayoría de las áreas aplicadas, apenas ahora se está empezando a aprovechar bien incluso la matemática de hace varios siglos

• Algún día los matemáticos podrían quedar sepultados bajo pruebas que revisar, y proposiciones falsas pero defendidas con exceso de confianza podrían entrar en la comunidad matemática. Los matemáticos del futuro quizá terminen como ingenieros de software que usan IA, revisando miles de líneas de pruebas generadas por IA en busca de errores sutiles

  • Ese momento ya llegó hace mucho. La literatura actual es inmensa y está llena de pruebas incorrectas, y entre los resultados publicados hay una cantidad desconocida, pero sin duda no cero, de resultados falsos mezclados