Un matemático rechaza el avance de la conjetura de OpenAI en 24 horas: "La IA demostró cada frase, pero ya no se trata de la conjetura original"

OpenAI afirmó que su modelo de IA de próxima generación resolvió diez problemas matemáticos de clase mundial, incluida la refutación de la conjetura de rigidez de Connes. Al día siguiente, una matemática humana respondió con un artículo argumentando que el contraejemplo de la IA es inválido. La autora, J. L. Nielsen, del Centro de Física Topológica de la Universidad de Kansas, rastreó las 37.000 líneas de código Lean 4 de OpenAI de principio a fin, mapeando cada objeto de vuelta a su prototipo matemático, e identificó dos vías de fallo independientes. La conjetura de rigidez de Connes establece que si dos grupos tienen la misma estructura algebraica asociada y satisfacen dos condiciones adicionales (ICC y la propiedad (T) de Kazhdan), entonces los grupos deben ser isomorfos. El modelo de OpenAI construyó dos grupos no isomorfos que generan la misma álgebra, con pruebas de que ambos grupos satisfacen ICC y la propiedad (T). Nielsen señaló que uno de los grupos construidos por la IA en realidad no satisfacía las condiciones adicionales, no siendo ni ICC ni teniendo la propiedad (T). Enumeró tres posibles razones: la representación de la propiedad (T) en el código no correspondía fielmente a la definición original de Kazhdan; la prueba solo se sostenía para una parte del grupo pero se aplicaba al todo; o el grupo en el código no es lo que describe el documento explicativo. Nielsen también realizó una verificación línea por línea del código, enumerando el nombre de cada objeto matemático y su número de línea en una tabla de referencia cruzada. Encontró que los lemas utilizados para probar ICC se aplicaban a objetos después de una transformación dual, no al grupo original con sus elementos centrales, por lo que no cubrían directamente los elementos críticos. Escribió sus dos refutaciones como código Lean y las compiló bajo Lean 4.32.2. La sección final del artículo discute el contexto más amplio: el núcleo de Lean garantiza la corrección formal, pero no si la afirmación realmente demuestra la conclusión prevista. Citando a Terence Tao, verificar una prueba comprueba la afirmación formal en sí misma, no su alineación con la intención, por lo que la revisión humana no puede ser reemplazada. Auditorías pasadas de cinco puntos de referencia comunes de Lean encontraron 4.833 problemas, incluidos contraejemplos, teoremas vacíos y axiomas poco fiables, todos verificados por máquina, y los humanos luego construyeron contraejemplos para mostrar que las afirmaciones demostradas eran falsas. Nielsen escribió que la formalización de OpenAI puede haber establecido correctamente cada conclusión que afirma, pero lo que no estableció—y lo que el núcleo de Lean no puede comprobar—es si estas conclusiones se relacionan con el enunciado original de la conjetura. La conjetura de rigidez de Connes sigue abierta.