La noche del 6 de octubre de 2026 apareció en GitHub una colección sorprendente. OpenAI publicó 722 manuscritos agrupados en 372 familias de resultados en un repositorio público. El productor se presenta como un modelo interno aún inédito. La ambición iguala la escala: 17 campos, desde la teoría de números y la geometría hasta la computación teórica y la física matemática. Este artículo clona el repositorio y lee el catálogo, los artículos y las trazas Lean para contar lo que hay de verdad. El anuncio OpenAI defiende un proceso transparente.
722 y 372 no nombran lo mismo. Un manuscrito es un documento único, mientras que una familia de resultados reúne los documentos que persiguen una misma meta: resultado principal, argumento compañero, aplicación o segunda prueba. El catálogo culmina en el número 377, con ausencias en 045, 061, 070, 123 y 163. El total real es por tanto 372. Las fechas van del 10 de septiembre al 6 de octubre; el 6 de octubre es solo el día de salida del catálogo. La instantánea examinada es el commit adc7f1241. La síntesis Kingy establece con claridad esta distinción.
Qué dicen los números
El régimen de producción se describe como uniforme. Tras saturar sus evaluaciones, el modelo afrontó unos 4.000 problemas abiertos. Las salidas que pasaron un filtro de importancia se agruparon en familias y manuscritos. Cada resultado habría exigido unas tres horas de reflexión ChatGPT Pro. Dos hilos quedan fuera de ese régimen: una zona sin ceros para zeta y Hodge para variedades abelianas CM. La redacción Re(s) > 11/12 fue pulida por humanos. No se publicó coste global alguno, ni número de tokens ni horas de acelerador. La síntesis CellCog señala abiertamente ese vacío.
La visita al repositorio tiene tres paradas. Primero el catálogo overview: fichas breves y enlaces de las 372 familias. Después el mapa CONTENTS: de la familia al artículo. Por fin las carpetas preprints: PDF, fuentes y datos de cita en cada una. La licencia es Apache 2.0. La disciplina de versiones se preserva, y cada corrección llega como nueva versión. Basta descargar un artículo; clonarlo todo pesa 2,4 GB y más de 130.000 archivos. El inventario BigChange confirma un PDF en cada una de las 722 carpetas.
Titulares destacados
El estante de teoría de números viene cargado. La familia 002 afirma la fórmula completa de Birch–Swinnerton-Dyer en corango bajo de Selmer, con finitud de Tate–Shafarevich. La familia 003 afirma un semiplano sin ceros Re(s) > 7/8 para funciones L de Dirichlet, más un segundo argumento para 11/12. La familia 005 afirma la irracionalidad de la constante de Catalan, mientras que la familia 017 afirma que el exponente de irracionalidad de pi vale 2. La convergencia de la serie de Flint–Hills figura en el mismo lote. Chowla en dos puntos y Deligne–Drinfeld también aparecen. El catálogo OpenAI los presenta como demostrados.
El ala de geometría y física es igual de amplia. La familia 032 entrega la tesis Hodge racional para variedades abelianas CM y productos K3, con consecuencias hacia Tate y el estándar de Hodge. Las conjeturas simétrica y general de Mahler forman la familia 087. Un contraejemplo a la finitud directa de Kaplansky en característica dos es la familia 197. La magnetización espontánea del ferromagneto cuántico de Heisenberg es 271, Vlasov–Maxwell relativista 3D es 362, y el isomorfismo de factores de grupos libres es 287. Cada uno exige una larga cadena de argumentos que a un humano le lleva semanas leer.
La computación teórica forma el bloque mayor con 40 familias. La conjetura de juegos únicos, la idea de que el azar no añade potencia en espacio logarítmico (L = RL = BPL), una cota 9/4 para el exponente de multiplicación de matrices, y multiplicación entera y transformada de Fourier bajo n log n se encuentran aquí. La no-amenabilidad del grupo F de Thompson, Hilbert–Smith, Kakeya en dimensiones 3 y 4, y la imposibilidad de colorear el plano con cinco colores bajo la regla de distancia unidad comparten el mismo estante. Según el recuento Kingy, la combinatoria sostiene 37 familias, la geometría 36 y la teoría de números 31. La amplitud también agranda la carga de verificación.
Verificación y debate
El frente de pruebas formales pide la lectura más prudente. Según el recuento CellCog, el resultado principal de 162 artículos dispone de formalización Lean. Documentos de alcance cubren 235 familias. La pila es enorme: unos 122.000 archivos Lean, 26 millones de líneas, con aporte de una treintena de proyectos externos. La comprobación pasa por Comparator, donde el enunciado desafiado y la solución viven en módulos separados. La marca sorry en un desafío no es una laguna sino el sustituto del enunciado a emparejar. El ejemplo dado desactiva nanoda y solo permite tres axiomas estándar. Las notas de estado dicen partial progress y unchecked. El examen BigChange subraya que esas notas son metadatos editoriales, no el resultado de un control ejecutado.
El debate de método pesa tanto como los resultados. El grupo independiente AGMAI, alojado en el IAS, reúne a nueve miembros, entre ellos Gowers, Witten, Hairer, Vakil y Wood. El 29 de septiembre, tras más de 600 respuestas, publicó principios: nada de sondear problemas avanzados en modelos cerrados, y difusiones construidas con la comunidad. La noche del 6 de octubre escribió que sus consejos no valen como aval y que la publicación abre el trabajo de comprensión humana. OpenAI anunció protocolos de revisión y cita, búsqueda de hospedaje comunitario y apoyo a talleres. La línea AGMAI es nítida: sin acceso igual, no hay investigación libre.
Una ruta práctica se impone al lector. Localizar la ficha de la familia en el catálogo overview y luego fijar el PDF y los datos de cita en su carpeta preprints: hash de commit, nombre de carpeta, versión. Cuando exista documento de alcance, anotar qué enunciado cubre Lean y qué queda fuera. Un paso Lean es una señal fuerte pero no una aceptación por sí sola; comprobar si el enunciado formal coincide con la tesis del artículo. El orden es catálogo, artículo, traza Lean, fuente independiente. No citar antes de verificar. OpenAI reitera su meta de difusión responsable del modelo; el AGMAI dice que la comunidad fijará la medida.
| Tema | Estado |
|---|---|
| 722 artículos, 372 familias | Catálogo abierto |
| 162 resultados Lean | Traza formal existe |
| Postura AGMAI | Sin aval por ahora |
Momentos clave
Comentario de la IA
"La escala impresiona, pero la ciencia se decide en la verificación. Esta síntesis lee catálogo y trazas Lean a nivel de versión para separar el anuncio de la señal real."
Evaluación de la IA
La contrapartida más fuerte nace de la propia escala. Cientos de tesis soltadas de golpe superan lo que la comunidad puede absorber. Sin arbitraje de pares, con un orden de cita nuevo y un historial breve. Por eso el texto AGMAI toma la difusión como un comienzo. El anuncio OpenAI insiste en el progreso. Esa tensión no se cerrará antes de la verificación.
Los límites son explícitos. OpenAI advierte que los resultados sin formalización pueden dar problemas. Incluso con traza Lean, el enunciado verificado no es todo el artículo. Citar sin leer la lista de exclusiones del documento de alcance es presentar como establecido lo que sigue abierto. Los relevamientos BigChange y CellCog recalcan esta distinción, mientras la síntesis Kingy trata las proporciones con prudencia: 372 sobre 4.000 no es una tasa de éxito verificada.
El interés plausible del autor es mostrar la potencia del modelo. La criba y el agrupado los hizo OpenAI, sin tabla de problemas descartados ni de intentos fallidos. Ello pone naturalmente los titulares brillantes por delante. El lector avanzará sabiendo que no todas las familias pesan igual. Los principios AGMAI tocan el mismo punto: sin herramientas abiertas a todos, la contienda no se juega en igualdad.
La lección práctica es directa. El matemático fijará la versión de su familia, inspeccionará el documento de alcance y la traza Lean, y comparará con fuentes independientes. El curioso partirá del catálogo overview, elegirá uno de los 10 resúmenes de razonamiento y pasará al artículo. Ambas vías comparten una regla: no citar antes de verificar.
Fuentes
7 enlaces; ninguna otra noticia publicada los cita. Stories sharing a link do not confirm each other; a source's origin is not inferred from how often it is cited.
inteligencia artificial · matemáticas · github · lean · pruebas · ciencia