El nuevo modelo de inferencia interno de OpenAI lanza diez avances matemáticos asombrosos de una sola vez.
Incluye:
- Se demostró por primera vez la existencia de grupos no soficos (non-sofic groups);
- Se han establecido nuevos límites inferiores de circuito (circuit lower bounds);
- Superó el límite de dificultad del Problema del Vector Más Cercano (Closest Vector Problem, CVP);
- Y el teorema de repetición paralela cuántica con decaimiento exponencial para juegos cuánticos bipersonales.
Lo que más le importa al profesor asociado de la Universidad de Columbia, Henry Yuen, es el último—
En 2016, Yuen logró avances significativos en este problema, pero no lo resolvió por completo. Durante 10 años, sufrió repetidos fracasos, e incluso hace un mes intentó nuevamente alcanzar la prueba definitiva con ChatGPT 5.5, obteniendo escasos resultados.
Y la IA, sobre su hombro, dio una suave patada, metiendo el balón en la portería.
La prueba está correcta, pero los humanos no lo entendieron.
Hace unos días, Lijie Chen envió un borrador del artículo a Henry Yuen y a otras personas.
En ese momento, su vida era muy ocupada y no tenía tiempo para estudiarlo a fondo. Ahora, el artículo ya se ha publicado. No puede quedarse callado; tiene cosas que decir.
El teorema de repetición paralela cuántica es el área en la que Henry Yuen dedicó años de esfuerzo durante su etapa de posgrado y también es su logro más orgulloso.
Henry Yuen, actualmente profesor asociado de ciencias de la computación en la Familia Srivani de la Universidad de Columbia
Él recordaba las tardes pasadas en cafés, las noches sentado en la oficina y innumerables fines de semana que deberían haber sido de descanso, descomponiendo y estudiando una y otra vez el teorema clásico de repetición paralela de Ran Raz.
Él quería resolver la versión cuántica de este teorema, por lo que no pudo dormir ni descansar. ingerió toneladas de herramientas matemáticas y finalmente logró demostrar la decadencia polinómica.
https://arxiv.org/pdf/1604.04340
Más importante aún, desarrolló confianza en sí mismo, finalmente reconoció su propio potencial y demostró que realmente podía resolver esos problemas (al menos parte de ellos) que también importan a otros.
Él cree que la prueba de OpenAI debería ser correcta, dado que ya existe una prueba formalizada en Lean. Sin embargo, Henry Yuen aún necesita algo de tiempo para comprender esta nueva prueba.
Aunque la nueva demostración efectivamente continúa desde donde él terminó anteriormente, la IA superó las limitaciones de su estrategia de demostración original, utilizando ciertas técnicas y métodos que posiblemente ya eran conocidos por investigadores en el campo de la teoría de operadores y el análisis funcional.
Además de la emoción, la primera reacción de Yuen fue la decepción, por el estilo de escritura del artículo.
Él dijo que este certificado parecía lleno de IA: una introducción larga y redundante que daba vueltas, mientras que los puntos clave eran como un truco de magia, dejando a uno confundido.
La prueba de OpenAI es interesante de leer, pero también algo complicada.
Primero coloca el problema claramente sobre la mesa, luego salta de repente hacia la dirección de "buscar la purificación correcta mediante pre-resolución", dejando casi ningún escalón lógico en el medio.
A continuación, se realizan una serie de cálculos de entropía de matriz bastante atípicos, que se desarrollan de forma compleja y finalmente te indican: este camino es viable.
Pero no explica de dónde proviene ese paso más crucial, esa intuición.
Y el movimiento más sutil y que más exige creatividad: la técnica de utilizar la transformación de Uhlmann para expandir el espacio de operadores, que debería haber sido el clímax más conmovedor de toda la demostración, fue descartada por la IA como arena y piedras, sin previo aviso ni explicación alguna, en la sección cuatro.
La prueba correcta, pero se escondió la idea más importante.
Él espera que OpenAI dedique más tiempo a los prompts para organizar bien este guion.
Lo que duele más es el segundo nivel: pasar la verificación de Lean no equivale a comprender.
La máquina puede garantizar que cada paso de la deducción sea impecable, pero no puede responder a preguntas como: «¿Por qué este método funciona?», «¿Qué significa en el panorama teórico más amplio?» o «¿Dónde más se puede aplicar?» — Lean no puede responder ninguna de estas.
Yuen admitió que aún está procesando esta prueba.
La respuesta está frente a él, pero él debe leerla como si fuera un artículo de un lego, línea por línea, para reconstruir la intuición que la IA no expresó.
Sí, hay una prueba de Lean ahí. Pero solo es una formalización, no significa que lo entienda. Para asimilarlo realmente, probablemente solo el tiempo lo irá moldeando.
Sí, la IA ha ampliado los límites de la comprensión humana, ¿pero qué queda luego? ¿Qué queda del placer y el significado de la investigación? ¿Qué le queda si la IA resuelve todos los problemas que lo han obsesionado?
Las preguntas se suceden. Pero una cosa se volvía cada vez más clara para él: los días siguientes del matemático no serían tranquilos; tendría que domar a estas bestias del pensamiento y traducir su jerga a lenguaje comprensible.
¡La IA "refuta" una conjetura matemática de cien años, ¡y se expone como falso! Lean tampoco es una caja fuerte
La semana pasada, Ramana Kumar refutó la famosa conjetura matemática no resuelta, la conjetura de Collatz, con 300 líneas de Lean.
La pregunta es muy sencilla: dado un número entero positivo, aplica repetidamente estas dos reglas: si es par, divídelo entre 2; si es impar, multiplícalo por 3 y suma 1. ¿Al final, sin importar desde qué número comiences, siempre terminarás llegando a 1?
Puedes calcularlo:
This conjecture states that no matter which positive integer you start with, you will eventually fall into the 4→2→1 cycle.
Since mathematician Lothar Collatz proposed it in 1937, no one has been able to prove it true or find a counterexample.
Fue llamado por el matemático Paul Erdős: «Las matemáticas aún no están listas para enfrentar este tipo de problemas», y el académico de la Academia Nacional de Ciencias de Estados Unidos, Jeffrey Lagarias, considera que «es un problema extremadamente difícil, completamente fuera del alcance de las matemáticas actuales».
If falsified, it would undoubtedly be a groundbreaking news in the mathematical community.
Lamentablemente, tres días después, esta prueba formal de Lean fue declarada inválida, ya que en realidad solo aprovechaba una vulnerabilidad subyacente del núcleo de Lean.
Daniel Selsam de OpenAI, con un AI especializado en ciberseguridad, ayudó a Lean FRO a realizar una auditoría del núcleo.
Como resultado, descubrieron más de una vulnerabilidad en el núcleo de Lean!
Casi al mismo tiempo, el profesor de matemáticas de la Universidad de Rutgers y asesor de la organización de investigación Lean, Alex Kontorovich, publicó una entrada recordando: no consideren a Lean como un verificador universal.
Él apunta directamente al punto débil: alineación semántica (Semantic Alignment).
Aunque el núcleo Lean sea impecable, Lean solo se encarga de la compilación del código. ¿Quién garantiza que la «definición» que escribes en el código sea lo mismo que la «intención intuitiva» humana expresada en lenguaje natural?
Lo único que Lean puede confirmar es que el código se compila correctamente y que la lógica formal es correcta. Pero no verifica un problema aún más crítico: ¿esta declaración formal realmente corresponde al teorema que deseas demostrar?
La demostración es correcta, pero el problema fue copiado mal, y Lean aún así da luz verde.
Y este problema de alineación no se puede resolver completamente con computadoras.
En la conferencia de ICM 2026, Kontorovich señaló que la mayor ceguera de las matemáticas formalizadas no está en "derivar correctamente", sino en "decir lo correcto". Al final, el control final debe ser realizado por expertos humanos.
El experimento de líquido tensorial se convirtió en leyenda precisamente gracias a la revisión manual casi obsesiva de cada definición matemática por parte de los investigadores.
Al poner juntas las palabras de los dos profesores, se apunta al mismo hecho: la IA puede demostrarlo, las máquinas pueden verificarlo, pero comprender y supervisar sigue siendo tarea humana.
Finalmente, hay un chisme sobre modelos de inferencia 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 canal de WeChat "Neozh Yuan", autor: Apocalipsis ASI; editor: David