OpenAI, el Principio de Partición y las Matemáticas
El lanzamiento por parte de OpenAI de cientos de demostraciones generadas por IA para difíciles problemas abiertos de matemáticas, muchas respaldadas por verificación formal en Lean pero escritas en una prosa opaca y torpe, está polarizando a la comunidad matemática. Los críticos argumentan que la empresa está usando las matemáticas como vehículo de relaciones públicas, trasladando el trabajo de verificación y exposición a investigadores ya sobrecargados y socavando normas establecidas de claridad, atribución y proceso científico. Los partidarios replican que los resultados formalmente verificados tienen un valor intrínseco, pueden refinarse con el tiempo y podrían acelerar el progreso matemático incluso si los resultados iniciales son confusos y difíciles de entender.
Carga sobre los matemáticos y “AI slop”
- Muchos ven el volcado de cientos de demostraciones generadas por IA, parcialmente incomprensibles, como un ataque de denegación de servicio contra expertos: un pequeño grupo de personas con las habilidades adecuadas queda inundado con artefactos que se les presiona social y profesionalmente para evaluar.
- Otros argumentan que “nadie está obligado” a leerlas; los críticos responden que las subvenciones, la publicidad y las constantes consultas de colegas y estudiantes hacen que, en la práctica, no involucrarse tenga un coste.
Validez y formalización en Lean
- Un bando afirma que las demostraciones verificadas en Lean, cuyas declaraciones formales coinciden con el problema objetivo, están entre los resultados matemáticos más fiables.
- Los contraargumentos señalan fallos concretos: una “refutación” de Collatz que aprovechaba un error del kernel de Lean, y resultados retractados con errores de signo. La verificación formal, las especificaciones y el código pueden ser erróneos o no coincidir.
- Varios dicen que leer la declaración en Lean es factible, pero los objetos de demostración son enormes y, en la práctica, ilegibles.
Legibilidad, exposición y la naturaleza de las matemáticas
- Una queja central: los artículos son poco claros, están estructurados de forma extraña y están mal citados; si los enviaran humanos, muchos serían rechazados sin revisión.
- Los matemáticos subrayan que las matemáticas no son solo verdad más certificado; la exposición, los nuevos métodos y la integración con la teoría existente son trabajo científico central.
- Otros responden que muchos artículos humanos son comparativamente malos, y que una prueba verdadera pero fea sigue siendo valiosa, solo que menos que una comprensible.
Las motivaciones de OpenAI y la estrategia de lanzamiento
- Quienes la defienden enmarcan el lanzamiento como apertura científica y una herramienta de evaluación; cualquiera interesado puede construir sobre los resultados.
- Los críticos ven sobre todo una maniobra de relaciones públicas: usar problemas abiertos para promocionar capacidades, ignorando recomendaciones del consejo (por ejemplo, sobre atribución, tasas de fallo y mejor exposición).
- Algunos califican el proceso de explotador: se necesita el trabajo de la comunidad para interpretar y depurar resultados que benefician principalmente a la empresa. También hay preocupaciones de que las salidas de la IA se parezcan mucho a trabajos no publicados enviados por usuarios.
Impacto en las carreras y los incentivos
- Los investigadores destacan el coste de oportunidad y un mercado laboral brutal: el tiempo empleado en descifrar artefactos de IA puede no ayudar a las carreras, especialmente a estudiantes y académicos sin plaza fija.
- Otros ven un “bufé” de nuevos resultados y lemas como oportunidades para que matemáticos ambiciosos los refinen, amplíen y mejoren.
El futuro de las matemáticas con IA
- Los entusiastas están entusiasmados: señalan proyectos comunitarios activos que mejoran cotas derivadas de la IA, imaginan repositorios automatizados de pruebas formales y esperan que los modelos futuros generen “pruebas agradables”.
- Los escépticos temen una “pérdida de significado”: humanos relegados a depurar o traducir pruebas ajenas, campos reorientados a verificar resultados de caja negra en lugar de desarrollar una comprensión compartida.