Conocimiento nuevo

Cuando la IA produce ciencia

Durante años la discusión fue si los modelos entienden o repiten. Hay un terreno donde esa pregunta se puede zanjar sin opinión: la matemática. Un resultado nuevo o es correcto o no lo es, y desde hace poco eso se puede verificar por máquina. En agosto de 2026 un modelo resolvió diez problemas que llevaban más de una década abiertos, y publicó las pruebas para que cualquiera las revise.

Ver el repositorio de papers Qué no significa →
La clave está en la verificación. Que un modelo afirme haber probado algo no vale nada por sí solo: podría estar alucinando con enorme elocuencia. Lo que cambió es que esas pruebas hoy se escriben en Lean, un lenguaje donde cada paso lógico lo revisa una computadora. Si el verificador acepta la prueba, es correcta. No hay lugar para la persuasión.
La línea de tiempo

De predecir proteínas a demostrar teoremas

2020 — 2021

AlphaFold y el plegamiento de proteínas

DeepMind resuelve un problema que la biología llevaba cincuenta años persiguiendo: predecir la forma tridimensional de una proteína a partir de su secuencia. Después libera las estructuras de 200 millones de proteínas en una base abierta que hoy usan más de tres millones de investigadores, desde vacunas contra la malaria hasta enzimas que degradan plástico. Fue la señal de que la IA podía acelerar la ciencia de manera irreversible.

2023 — 2024

Materiales y las primeras demostraciones formales

GNoME amplía enormemente el catálogo de materiales estables conocidos. En paralelo aparecen AlphaProof y AlphaGeometry, que no solo resuelven problemas de olimpíada a nivel de medalla sino que formalizan sus pruebas en Lean: la máquina no solo responde, también demuestra que su respuesta es válida. Ahí nace el circuito que importa.

2025

AlphaEvolve mejora récords de décadas

Un sistema evolutivo guiado por modelos de lenguaje encuentra un algoritmo de multiplicación de matrices mejor que el récord vigente desde hacía 56 años, y mejora cotas en varias áreas de la matemática. Ya no se trata de resolver ejercicios conocidos: es encontrar construcciones que ningún humano había encontrado.

Agosto 2026

Astra y diez problemas abiertos

OpenAI presenta su próximo modelo, Astra, de una manera inusual: no lo lanza. En su lugar publica soluciones a diez problemas sin resolver desde hace diez años o más, con un manuscrito de 249 páginas y los certificados de prueba en Lean 4 en un repositorio abierto. Entre los resultados: la construcción explícita de un grupo no-sófico —pregunta abierta desde que Gromov planteó el concepto en 1999—, la refutación de la conjetura de rigidez de Connes, la conjetura de volumen de Ehrhart y tres problemas del catálogo de Erdős. El cómputo de las diez soluciones costó unos US$2.000.

Por qué es distinto

Tres cosas que cambian con esto

Verificación La prueba no se discute: se corre Un texto persuasivo puede estar equivocado; una prueba formal aceptada por el verificador, no. Que el repositorio de Astra no tenga ningún paso pendiente significa que la máquina revisó la cadena lógica completa. Es la primera vez que la pregunta "¿de verdad lo resolvió?" tiene una respuesta que no depende de la reputación de nadie. Lean 4 · pruebas auditables por cualquiera
Costo Dos mil dólares Ese fue el gasto de cómputo de las diez soluciones. Décadas de trabajo humano acumulado frente a un presupuesto menor al de un viaje a un congreso. Si el número se sostiene en resultados futuros, cambia menos quién puede investigar que cuántos intentos puede permitirse antes de abandonar una línea de trabajo. Costo de cómputo declarado por OpenAI
El nuevo cuello de botella Formular la pregunta Si generar y verificar demostraciones se abarata, el trabajo escaso pasa a ser otro: decidir qué vale la pena preguntar, traducir un problema difuso del mundo a una formulación tratable y juzgar si el resultado importa. Eso sigue siendo profundamente humano, y es exactamente el tipo de criterio que ninguna herramienta reemplaza. De ejecutar a dirigir la investigación
Con los pies en la tierra

Qué no significa

Un resultado espectacular invita a conclusiones apresuradas. Estas son las que conviene evitar.

No es que la IA reemplace a los matemáticos Los diez problemas fueron elegidos, formalizados y evaluados por personas. La formalización en Lean —traducir un enunciado matemático a algo que una máquina pueda verificar— es en sí misma un trabajo experto y costoso. El modelo aportó la búsqueda; el marco lo puso la comunidad.
No toda la ciencia se verifica así La matemática tiene una ventaja rara: su verdad es formalizable. En biología, medicina o ciencias sociales no hay un verificador que diga "correcto"; hay experimentos, réplicas y discusión. Estos resultados no se trasladan de manera directa a disciplinas donde la evidencia es empírica.
Anunciar no es publicar Astra no está disponible: no hay fecha, ni precio, ni model card, ni acceso. Lo que se publicó son resultados y pruebas, no el sistema que los produjo. Es un anuncio con evidencia fuerte, pero sigue siendo un anuncio, y la revisión de la comunidad matemática recién empieza.
Diez problemas no son la matemática Son diez preguntas concretas, difíciles y acotadas, en áreas donde la búsqueda automatizada rinde bien. Enorme como hito; modesto frente al conjunto de la disciplina. Conviene celebrarlo por lo que es y no por lo que sugiere el titular.

Lo que se mide y lo que se demuestra

Durante dos años discutimos benchmarks saturados y puntajes autorreportados. Este es el contraste: un resultado que cualquiera puede verificar por su cuenta. Para entender cómo se mide todo lo demás, pasá por la sección de benchmarks.

Cómo se mide un modelo →Ver la actualidad