El último modelo de razonamiento interno de OpenAI ha logrado diez avances matemáticos sorprendentes de una vez.
Entre ellos se incluyen:
- La primera prueba de la existencia de grupos no soficos (Non-sofic groups);
- Nuevos límites inferiores para circuitos (Circuit lower bounds);
- La superación del límite de dificultad del problema del vector más cercano (Closest Vector Problem, CVP);
- Y el teorema de decaimiento exponencial de la repetición paralela cuántica en juegos de dos jugadores (Quantum parallel repetition).
El que más le importa al profesor asociado de la Universidad de Columbia, Henry Yuen, es el último.
En 2016, Yuen logró un progreso significativo en este problema, pero no lo resolvió por completo. Durante 10 años, fracasó repetidamente, e incluso hace un mes usó ChatGPT 5.5 para intentar nuevamente alcanzar la prueba definitiva, pero obtuvo pocos resultados.
Y la IA, apoyándose en sus hombros, con un toque suave, metió el gol.
La prueba es correcta, pero la humanidad no la entiende
Hace unos días, Lijie Chen envió a Henry Yuen y a otras personas un borrador de un artículo.
En ese momento estaba muy ocupado con la vida y no tuvo tiempo de profundizar en su lectura. Ahora, el artículo ya se ha publicado. No puede evitar hablar y tiene algo que decir.
El teorema de repetición paralela cuántica (Quantum parallel repetition theorem) es un campo en el que Henry Yuen invirtió años de esfuerzo durante sus estudios de posgrado, y también es su logro más preciado.
Henry Yuen, actual profesor asociado de Ciencias de la Computación Srivani Family en la Universidad de Columbia.
Recuerda esas tardes pasadas en cafeterías, las noches profundas en la oficina y los incontables fines de semana que deberían haber sido de descanso, desarmando y estudiando repetidamente el clásico teorema de repetición paralela de Ran Raz.
Quería resolver la versión cuántica de este teorema, lo que le causó insomnio y ansiedad. Se tragó toneladas de herramientas matemáticas y finalmente logró probar el decaimiento polinomial.
https://arxiv.org/pdf/1604.04340
Lo más importante es que, a partir de esto, construyó confianza, finalmente reconoció sus propias capacidades y demostró que realmente podía resolver esos problemas (al menos algunos) que a otros también les importaban.
Cree que la prueba de OpenAI debe ser correcta, después de todo ya existe una prueba formalizada en Lean. Pero para digerir esta nueva prueba, Henry Yuen aún necesita algo de tiempo.
Aunque la nueva prueba efectivamente continúa desde donde él dejó, la IA superó las limitaciones de su estrategia de prueba original, utilizando algunos trucos y métodos. Es posible que estos métodos ya sean conocidos por investigadores en teoría de operadores (operator theory) y análisis funcional (functional analysis).
Además de la emoción, el primer sentimiento de Yuen fue decepción, decepción con el estilo de redacción del artículo.
Dice que esta prueba se lee como escrita por una IA: introducciones larguísimas que dan vueltas, pero los pasos clave aparecen como por arte de magia, dejando a uno desconcertado.
La prueba de OpenAI es interesante de leer, pero también algo desconcertante.
Primero coloca el problema cuidadosamente sobre la mesa, y luego salta repentinamente a la dirección de "usar la resolvente para encontrar la purificación correcta", dejando casi ningún escalón lógico intermedio.
Lo que sigue es una serie de cálculos de entropía matricial bastante inusuales, que continúan con rodeos, y al final te dicen: este camino funciona.
Pero ese paso crucial, de dónde viene exactamente la intuición, no lo dice.
Y el toque más ingenioso y creativo—la técnica de expansión del espacio de operadores utilizando la transformación de Uhlmann (Uhlmann transformation), que debería ser el clímax más emocionante de toda la prueba— fue descartado por la IA sin previo aviso y sin explicación, arrojado en la sección cuatro.
La prueba es correcta, pero esconde la idea más importante.
Espera que OpenAI pueda gastar algunos prompts más para organizar bien este manuscrito.
Lo que duele aún más es la segunda capa: que Lean verifique no significa comprender.
La máquina puede garantizar que cada paso de deducción es impecable, pero preguntas como "por qué funciona este truco", "qué significa en el panorama teórico más amplio", "dónde más se puede aplicar"—Lean no puede responder a ninguna de estas.
Yuen admite que todavía está digiriendo esta prueba.
La respuesta está frente a él, pero tiene que reconstruir línea por línea la intuición no expresada por la IA, como si leyera un artículo de un profano.
Sí, hay una prueba en Lean ahí. Pero eso es solo formalización, no significa que yo lo entienda. Para digerirlo realmente, probablemente solo pueda confiar en que el tiempo lo irá puliendo lentamente.
Ciertamente, la IA ha ampliado las fronteras de la comprensión humana, pero ¿y luego? ¿Qué queda del placer y el significado de la investigación? Si la IA resuelve todos los problemas que le quitan el sueño, ¿qué le queda a él?
Las preguntas se suceden. Pero hay algo de lo que está cada vez más seguro: los matemáticos no se quedarán ociosos en los próximos días; tendrán que domesticar a estas bestias de pensamiento y también traducir su jerga a un lenguaje humano.
¡La "refutación" de una conjetura matemática centenaria por una IA es desacreditada! Lean tampoco es una caja fuerte
La semana pasada, Ramana Kumar usó 300 líneas de Lean para refutar la conjetura matemática no resuelta más famosa, la "Conjetura de Collatz" (Collatz conjecture).
La pregunta que plantea es particularmente simple: te dan un entero positivo, aplicas dos reglas repetidamente—si es par, divides por 2; si es impar, multiplicas por 3 y sumas 1— ¿finalmente, sin importar desde qué número empieces, siempre caerás hasta el 1?
Puedes calcularlo:
Lo que dice esta conjetura es: sin importar con qué entero positivo comiences, eventualmente caerás en este ciclo 4→2→1.
Desde que el matemático Lothar Collatz la planteó en 1937, nadie ha podido demostrar que sea cierta, ni ha encontrado un contraejemplo.
El matemático Paul Erdős la llamó: "Las matemáticas aún no están preparadas para problemas así", y el miembro de la Academia Nacional de Ciencias de EE. UU. y matemático Jeffrey Lagarias considera que "es un problema excepcionalmente difícil, completamente fuera del alcance de las matemáticas actuales".
Si fuera refutada, sin duda sería una noticia explosiva en el mundo matemático.
Lamentablemente, 3 días después, esta prueba formalizada en Lean fue declarada inválida, porque en realidad solo aprovechó una vulnerabilidad de bajo nivel en el núcleo de Lean.
Daniel Selsam de OpenAI, junto con una IA especializada en seguridad cibernética, ayudó a Lean FRO a realizar una auditoría del núcleo.
¡El resultado fue que encontraron no una, sino varias vulnerabilidades en el núcleo de Lean!
Casi al mismo tiempo, Alex Kontorovich, profesor de matemáticas de la Universidad de Rutgers y asesor del grupo de investigación especializado en Lean, publicó un mensaje advirtiendo: no trates a Lean como un verificador infalible.
Señaló directamente el punto débil—la alineación semántica (Semantic Alignment).
Incluso si el núcleo de Lean fuera impenetrable, Lean solo se encarga de compilar el código. ¿Quién asegura que las "definiciones" que escribes en el código corresponden a la "intención intuitiva" humana en lenguaje natural?
Lo único que Lean puede confirmar es: el código se compila correctamente, la lógica formal es impecable. Pero no verifica un problema más crucial: ¿esta afirmación formalizada realmente corresponde al teorema que quieres demostrar?
Si el teorema se demuestra correctamente pero el enunciado del problema está mal escrito, Lean igual dará luz verde.
Y este problema de alineación no puede resolverse únicamente con computadoras.
En su charla en el ICM 2026, Kontorovich ya había señalado: el punto ciego más grande de las matemáticas formalizadas no está en "deducir correctamente", sino en "decir lo correcto". Los que tienen la última palabra todavía deben ser los expertos humanos.
El Experimento del Tensor Líquido (Liquid Tensor Experiment) se convirtió en leyenda precisamente por la revisión humana casi obsesiva de cada definición matemática por parte de los investigadores.
Colocando las palabras de los dos profesores juntas, apuntan al mismo hecho: la IA puede probar, la máquina puede verificar, pero comprender y supervisar sigue siendo trabajo humano.
Finalmente, hay un rumor sobre los modelos de razonamiento de IA:
Referencias:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Este artículo proviene del WeChat público "新智元" (Nueva Era de la Inteligencia), autor: ASI启示录; editor: David
