Terence Tao y la 'Big Mathematics': IA que demuestra teoremas

La inteligencia artificial ya no solo escribe código: ahora demuestra teoremas, resuelve problemas de olimpiada y verifica pruebas que antes tomaban años de trabajo humano. La IA en matemáticas dejó de ser una curiosidad de laboratorio para convertirse en una herramienta de investigación real, usada por algunos de los mejores matemáticos del mundo.

Un reportaje de IEEE Spectrum publicado el 25 de junio de 2026 recoge el debate que esto abre entre los propios protagonistas: si una máquina puede hallar la demostración, ¿qué significa hoy ser matemático?

TL;DR

• IEEE Spectrum publicó el 25 de junio de 2026 un reportaje de Benjamin Skuse sobre el papel del matemático en la era de la IA.
• Terence Tao (UCLA) plantea una era de Big Mathematics: humanos y máquinas colaborando en problemas complejos.
• AlphaProof y AlphaGeometry2 de DeepMind alcanzaron nivel de medalla de plata en la IMO 2024 con 28 de 42 puntos.
• El asistente de pruebas Lean y su librería Mathlib superan el millón de líneas de matemática formalizada y verificada.
• Tao y colaboradores formalizaron la conjetura PFR en Lean en unas tres semanas a fines de 2023.
• En el benchmark FrontierMath los mejores modelos resolvían menos del 2% de los problemas al lanzarse en 2024.
• El debate de fondo no es técnico sino humano: la motivación, el sentido y la belleza de entender una demostración.

Qué pasó: la IA en matemáticas reabre una vieja pregunta

El reportaje de IEEE Spectrum, firmado por el divulgador y exdoctorando en matemática aplicada Benjamin Skuse, no anuncia un nuevo récord ni un teorema resuelto por sorpresa. Hace algo menos llamativo pero más profundo: pregunta a matemáticos en activo qué sienten ahora que parte de su trabajo puede automatizarse. La pieza enfrenta dos miradas que conviven en la comunidad. Por un lado, el optimismo de quienes ven a la IA en matemáticas como un multiplicador de capacidades. Por el otro, la cautela de quienes temen que el oficio pierda lo que lo hacía valioso.

La figura central es Terence Tao, matemático de la Universidad de California en Los Ángeles y ganador de la Medalla Fields, quizá el matemático vivo más influyente. Tao describe la llegada de una era de Big Mathematics (matemática a gran escala), por analogía con la big science: grandes colaboraciones donde humanos y máquinas atacan juntos problemas que antes requerían comunidades enteras durante décadas. En su visión, la máquina no expulsa al matemático del problema; lo libera de la parte mecánica para que se concentre en las ideas, las conjeturas y la estrategia.

Frente a ese entusiasmo, el reportaje da espacio a una reflexión más íntima de Jeremy Avigad, matemático y lógico de la Universidad Carnegie Mellon. Avigad recuerda que el motor de la matemática nunca fue solo resolver: fue entender. "A veces, la comprensión simplemente te golpea como algo muy hermoso", dice. "A veces es una sensación de logro, como terminar un maratón. Pero no es exactamente ninguna de las dos: es una sensación maravillosa cuando llevas mucho tiempo pensando en algo complejo y difícil y, de repente, todo encaja". Esa frase resume la tensión del artículo: si la IA entrega el resultado sin el viaje, ¿se pierde también el sentido?

La demostración como proceso humano, no solo como resultado.

Contexto e historia: de las cuatro colores a Lean

La idea de una máquina ayudando a probar teoremas no es nueva. En 1976, el teorema de los cuatro colores se convirtió en el primer gran resultado demostrado con ayuda esencial de una computadora, que verificó cientos de casos imposibles de revisar a mano. Aquello generó un debate filosófico que todavía resuena: ¿es una demostración "real" si ningún humano puede leerla completa? Décadas después, el proyecto Flyspeck formalizó por completo la prueba de la conjetura de Kepler sobre el empaquetamiento de esferas, sellando con verificación mecánica un resultado que muchos dudaban en aceptar.

Lo que cambió en los últimos años es la madurez de los asistentes de pruebas y la irrupción de los modelos de lenguaje. Un asistente de pruebas como Lean es, en esencia, un lenguaje de programación donde cada paso de un argumento matemático se escribe como código que el sistema verifica de forma rigurosa. Si la prueba tiene un hueco, el programa no compila. Sobre Lean se construyó Mathlib, una biblioteca colaborativa que ya supera el millón de líneas de matemática formalizada: desde aritmética básica hasta análisis funcional y teoría de categorías.

Aquí entra la IA generativa. Los modelos modernos pueden proponer borradores de pruebas en lenguaje natural, traducirlos a Lean y corregir los errores que el verificador señala, en un ciclo de prueba y error mucho más rápido que el humano. La IA en matemáticas no reemplaza al verificador formal: lo alimenta. La máquina conjetura y redacta; Lean dice si está bien.

📌 Nota: Un asistente de pruebas no "confía" en la IA. Aunque un modelo genere una demostración convincente pero falsa, Lean la rechaza si un solo paso no se sostiene. Esa es su garantía clave.

Datos y cifras: lo que las máquinas ya resuelven

Los números ayudan a dimensionar el salto. En julio de 2024, los sistemas AlphaProof y AlphaGeometry2 de Google DeepMind resolvieron cuatro de los seis problemas de la Olimpiada Internacional de Matemáticas (IMO), sumando 28 de 42 puntos: nivel de medalla de plata, a un solo punto del oro. Era la primera vez que una IA alcanzaba ese rendimiento en la competencia matemática preuniversitaria más exigente del mundo. AlphaProof trabajaba precisamente formalizando los problemas en Lean y buscando demostraciones verificables.

En el terreno de la investigación, el propio Tao lideró a fines de 2023 la formalización en Lean de la conjetura polinomial de Freiman-Ruzsa (PFR), recién demostrada en papel. Lo que en otra época habría tomado meses se completó, con una comunidad coordinada, en alrededor de tres semanas. Fue una demostración de que la formalización asistida ya es práctica, no solo teórica.

Al mismo tiempo, los límites siguen siendo claros. El benchmark FrontierMath, presentado por Epoch AI a fines de 2024 con problemas originales de nivel investigación, mostró que los mejores modelos del momento resolvían menos del 2% de los ejercicios. La matemática de frontera, la que realmente importa, todavía está mayormente fuera del alcance autónomo de la IA.

De la conjetura humana a la verificación formal en Lean.

Impacto y análisis: ¿reemplazo o copiloto?

Para entender por qué la IA en matemáticas entusiasma a investigadores como Tao, conviene ver cómo luce una demostración formal. Tomemos algo elemental: probar que la suma de números naturales es conmutativa. En Lean 4 se escribe así, y el sistema verifica cada paso:

-- Lean 4: demostración formal de que la suma es conmutativa
theorem suma_conmutativa (a b : Nat) : a + b = b + a := by
  induction b with
  | zero => simp
  | succ n ih => rw [Nat.add_succ, ih, Nat.succ_add]

Cada línea es un paso lógico que la máquina valida sin margen de error. Ahora imaginemos miles de teoremas encadenados: ese es Mathlib. Y la IA puede aprender de ese corpus para sugerir el siguiente paso, igual que un copiloto de código sugiere la siguiente línea. El flujo de trabajo se parece cada vez más al desarrollo de software:

graph LR
  A["Matemático: conjetura"] --> B["IA: genera demostración"]
  B --> C["Lean: verifica paso a paso"]
  C -->|"falla"| B
  C -->|"válida"| D["Teorema certificado"]

Para un desarrollador en LATAM, la analogía es directa: la IA en matemáticas funciona como un test runner combinado con un asistente de autocompletado. El humano define qué quiere probar (la especificación), la IA propone una implementación (la demostración) y el verificador actúa como una suite de tests que no acepta atajos. Quien programe con TDD reconocerá el patrón de inmediato.

💭 Clave: El miedo de Avigad no es que la IA se equivoque, sino que acierte demasiado. Si la máquina entrega el resultado sin el esfuerzo, desaparece el aprendizaje que forma matemáticos. Es el mismo debate que hoy enfrenta el desarrollo de software con los asistentes de código.

Ese paralelo no es casual. El propio reportaje conecta con una discusión que la industria tech ya conoce: cuando una herramienta resuelve la parte difícil, los novatos pierden la oportunidad de tropezar, batallar y aprender. En programación se discute si los asistentes de IA degradan la comprensión profunda del código; en matemática, la pregunta es si las nuevas generaciones desarrollarán la intuición que solo nace de pasarse años atascados en un problema.

Qué sigue: la era de la "Big Mathematics"

El escenario que dibuja Tao apunta a una colaboración masiva. Con asistentes de pruebas, miles de matemáticos pueden trabajar sobre una misma demostración formal sin temor a que un error se cuele, porque el sistema garantiza la consistencia. La IA actúa como pegamento: rellena pasos rutinarios, traduce entre el lenguaje informal y el formal, y busca contraejemplos. El resultado podría ser un ritmo de descubrimiento inédito, con proyectos colaborativos a escala que hoy serían inmanejables.

Para la comunidad hispanohablante, esto abre una puerta concreta. Aprender Lean ya no es un ejercicio académico aislado: es una habilidad puente entre matemática, verificación formal y desarrollo de software seguro, un área donde LATAM tiene talento de sobra y poca representación. Las mismas técnicas de verificación formal que validan teoremas se usan para certificar que un microkernel, un contrato inteligente o un protocolo criptográfico no tienen fallos.

💡 Tip: Si querés experimentar, Lean 4 es gratuito y open source. Empezá por el tutorial interactivo Natural Number Game, que enseña a demostrar teoremas como si fuera un videojuego, sin necesidad de instalar nada.

Lo que ninguna de las dos posturas niega es que el oficio cambiará. La discusión real, la que plantea IEEE Spectrum, no es si la IA en matemáticas será útil —ya lo es— sino qué parte del trabajo seguirá teniendo sentido hacer a mano. Y esa pregunta, paradójicamente, es de las pocas que ninguna máquina puede responder por nosotros.

📖 Resumen en Telegram: Ver resumen

Preguntas frecuentes

¿La IA ya puede demostrar teoremas por sí sola?

Parcialmente. Sistemas como AlphaProof resuelven problemas de olimpiada a nivel de medalla de plata y la IA ayuda a formalizar demostraciones reales en Lean. Pero en matemática de frontera, los mejores modelos resolvían menos del 2% del benchmark FrontierMath en 2024. La IA es hoy un asistente potente, no un sustituto autónomo.

¿Qué es un asistente de pruebas como Lean?

Es un lenguaje de programación donde cada paso de una demostración matemática se escribe como código que el sistema verifica con rigor absoluto. Si un paso no se sostiene, no compila. Eso garantiza que una prueba aceptada por Lean es lógicamente correcta, incluso si fue redactada por una IA.

¿Qué significa la "Big Mathematics" de Terence Tao?

Es la visión de una matemática a gran escala, por analogía con la big science: grandes colaboraciones entre humanos y máquinas atacando problemas complejos. La IA y los asistentes de pruebas permiten coordinar a muchos matemáticos sobre una misma demostración sin que se acumulen errores.

¿Por qué algunos matemáticos están preocupados?

Porque el valor del oficio nunca fue solo el resultado, sino la comprensión que nace del proceso. Jeremy Avigad teme que, si la máquina entrega la respuesta sin el esfuerzo, las nuevas generaciones pierdan la intuición y el sentido que solo se desarrollan batallando con un problema durante años.

¿Sirve aprender Lean si soy desarrollador y no matemático?

Sí. Las técnicas de verificación formal de Lean se aplican a software crítico: kernels, contratos inteligentes y protocolos criptográficos. Aprenderlo conecta matemática, lógica y desarrollo seguro, un perfil muy demandado y escaso en LATAM.

Referencias

• IEEE Spectrum — Reportaje original de Benjamin Skuse sobre el rol del matemático cuando la IA hace el cálculo.
• Lean 4 (GitHub) — Repositorio oficial del asistente de pruebas Lean.
• Blog de Terence Tao — Notas del matemático sobre formalización en Lean y el proyecto PFR.
• Google DeepMind — Anuncio de AlphaProof y AlphaGeometry2 en la IMO 2024.
• FrontierMath (arXiv) — Benchmark de problemas matemáticos de nivel investigación.

📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.