OpenAI retira tres resultados matemáticos de su repositorio

Entonces, ¿las 3 pruebas retiradas eran las que no tenían verificación en Lean?

Si es así, ¿por qué mezclaron pruebas verificadas con Lean y pruebas en lenguaje natural?

Me preguntaba eso mientras leía el blog de Aaronson:

https://scottaaronson.blog/?p=10169

O al menos, ¡estamos bastante seguros de que es una prueba! Hay un certificado Lean, como lo hay para algunos de los otros 372 resultados revolucionarios (no para todos). Pero también parece que ningún humano ha entendido casi ninguna de estas pruebas todavía

Parece que lo obvio sería publicar en DOS partes: las que están verificadas y las que podrían tener algunas buenas ideas pero también algunos errores. Presumiblemente, las últimas serían mucho más costosas de verificar para los humanos.

Creo que, tras un examen más detenido, muchas de estas pruebas totalmente generadas por IA se desmoronarán. Incluso en Lean, puedes construir teorías que compilan pero que, no obstante, afirman algo diferente de lo que realmente pretendes. Es solo que el volumen de pruebas es tan asombrosamente grande que probablemente pasarán años antes de que encontremos los problemas, como con la conjetura abc.

El artículo sobre superar O(n log n) para la multiplicación de enteros también me parece bastante sospechoso; no estoy seguro, pero parece demasiado bueno para ser verdad. Siento que debe haber un fallo sutil en eso. Quizás sea solo que odio esos números pequeños en el artículo, ¡pero parece incorrecto, antinatural incluso! Sería igualmente escéptico ante un artículo de física que afirme poder superar la velocidad de la luz por una fracción diminuta. No hay razón para que n log n sea el límite natural aquí, pero veo algunas buenas intuiciones, así que tener algo más que no pueda representarse en una forma elegante me parece muy poco matemático.

Si haces un volcado como este, todo debería estar formalizado; simplemente hay demasiado material para revisar a mano y, además, está escrito por IA, lo que lo hace difícil de leer en comparación con el trabajo humano.

Qué época, el modelo de OpenAI es tan bueno que publica cientos de artículos de matemáticas.

¡¡¡El último modelo incluso encuentra errores en artículos de matemáticas publicados previamente!!!*

* hasta ahora, solo los artículos de matemáticas de OpenAI eran defectuosos y necesitaban retractación.

Así se ve cuando las prácticas de ingeniería de software se encuentran con las matemáticas. "openai/math release 1.3.42: retractados los artículos 139 y 140, corregido un error de signo en el artículo 47, restaurado el artículo 85 previamente retractado, refactorizados los argumentos en el artículo 101".

Tengo curiosidad por saber si la retirada se debió a que un matemático real miró los artículos y notó los errores, o si pasaron un modelo por ellos para corregirlos, lo cual no sería la primera vez, presumiblemente, ya que seguramente lo habrían hecho antes de publicar. Ambas opciones tienen implicaciones interesantes.

3 errores (hasta ahora) de ~400 sigue siendo una tasa de acierto bastante buena

Así que las matemáticas han entrado en la fase de "lanzar cosas a una pizarra y ver si se pegan"...

Esto es solo OpenAI robando más trabajo.

No tengo problema con que publiquen. No tengo problema con el proceso y cómo interactúan con él. Me encanta que actúen como administradores de estos trabajos.

Aparte de todo eso, deberían pagar a las personas que verifican los problemas. Lo que realmente me molesta es que sabemos que cualquier cosa publicada en el proceso de verificación de esto va a ser absorbida en la próxima sesión de entrenamiento.