GPT-5.6 usó un prompt para cerrar una brecha de 30 años en optimización convexa
Un modelo de IA (GPT‑5.6 “Sol Pro”) ha ayudado a demostrar un resultado abierto de 30 años en optimización convexa, usando un prompt experto de diez páginas y una demostración verificada después en el teorema provador Lean. Los comentaristas debaten cuánta novedad genuina aportó el sistema frente a actuar como un asistente automatizado extremadamente poderoso, y qué implica esto para el futuro papel de matemáticos y programadores, especialmente en problemas de “frutos bajos y medios”. El hilo se amplía hacia preguntas sobre si los grandes modelos de lenguaje son solo “loros estocásticos”, cuán rápido podrían desplazar trabajo humano en distintos campos y qué cambios sociales y económicos harían falta si la IA sigue avanzando.
Alcance del resultado y cómo se obtuvo
- Los comentaristas señalan que la demostración está verificada en Lean, pero aún no ha pasado por revisión por pares, así que su estado es “prometedor pero provisional”.
- El matiz clave: GPT‑5.6 Sol Pro usó un prompt de ~10 páginas, elaborado por expertos del dominio, construido sobre un año de trabajo humano previo (incluidos intentos anteriores asistidos por LLM).
- Esto se ve como una fuerte evidencia de que los LLM pueden cerrar brechas cuando el camino es alcanzable con técnicas existentes, pero no como una autonomía tipo “escribe ‘resuelve esto’ y vete”.
Implicaciones para las carreras en matemáticas e investigación
- Algunos argumentan que los frutos bajos y “medios” en matemáticas/TCS se transferirán cada vez más a la IA, dejando a los humanos centrarse en ideas verdaderamente novedosas y en la चयन de problemas.
- Otros temen que esto socave las rutas tradicionales de formación, donde los principiantes se curtían con este tipo de problemas.
- Varios comparan esto con el software: los juniors y quienes “siguen recetas” podrían ser desplazados primero; la comprensión profunda del dominio y de sistemas sigue importando.
LLMs: inteligencia, creatividad y debate sobre el “loro estocástico”
- Los entusiastas dicen que resolver problemas de 30 años y contribuir a otras conjeturas refuta la visión de “mero loro” y muestra razonamiento genuino.
- Los escépticos mantienen que los LLM son motores sofisticados de predicción construidos sobre patrones generados por humanos, no verdaderamente creativos ni con comprensión real.
- Algunos sugieren que, si esto no es “inteligencia”, la palabra pierde significado; otros responden que el emparejamiento estadístico de patrones más la búsqueda por fuerza bruta pueden explicarlo.
Prompting, agentes e “ingeniería del harness”
- Varios comentarios subrayan que escribir buenos prompts y procesos se parece más a la ingeniería de procesos/harness que a un “prompting mágico”.
- Hay discusión sobre sistemas multiagente (Pro vs Ultra), donde los modelos planifican, ejecutan, prueban y se autocritican en bucles.
- La gente señala que los LLM también pueden ayudar a generar sus propios prompts y flujos de trabajo, reduciendo con el tiempo la necesidad de artesanía manual en prompts.
Verificación formal e infraestructura de demostraciones
- Lean se destaca como el análogo actual de sistemas más antiguos como Mizar; las pruebas verificadas por máquina se consideran cruciales para confiar en las matemáticas generadas por IA.
- A algunos les gustaría ver a los LLM abordar demostraciones muy largas u opacas (por ejemplo, grandes teoremas de clasificación) mediante formalización completa.
Preocupaciones sociales y económicas más amplias
- Las reacciones van desde la emoción (“la inteligencia es barata, podemos acelerar la ciencia”) hasta la ansiedad por la pérdida de empleo, la estratificación y futuros “tecnofeudales”.
- Varios sostienen que el verdadero problema es la economía política: cómo se distribuyen las ganancias, no las matemáticas en sí.