Mil agentes de IA y una demostración: qué muestra realmente el experimento con Lean
Cuando mil agentes de IA trabajan en un mismo problema, el modelo es solo una parte del sistema. La otra es cómo reparten el trabajo, comparten el estado, proponen cambios y comprueban si un resultado es válido.
El 9 de noviembre, Anthropic describió un experimento en el que unos 1.000 agentes con una versión inicial de Claude Fable 5.2 reprodujeron una demostración formal del último teorema de Fermat en el asistente de pruebas Lean. La empresa afirma que la ejecución tardó 28,7 horas. Es un experimento de investigación comunicado por la propia empresa, no una referencia universal para equipos de software.
La primera distinción importa: los agentes no descubrieron el último teorema de Fermat ni sustituyeron la demostración de Andrew Wiles. La tarea consistía en formalizar un resultado matemático existente para que un asistente de pruebas pudiera comprobar sus pasos. Es un trabajo matemático y de ingeniería considerable, pero distinto de inventar una demostración nueva.
El equipo tenía un mapa y herramientas
Según el informe técnico de Anthropic, los agentes recibieron 60 enunciados para demostrar: 59 hitos intermedios y el propio teorema. También recibieron un breve esquema de la ruta clásica, definiciones relevantes y 47 lemas ya demostrados en la formalización anterior del equipo. Esas entradas forman parte del resultado; los agentes no partieron de una página en blanco.
Los investigadores asignaron un agente líder y 999 auxiliares. Cada agente tenía su propio entorno aislado, una consola, un editor de archivos, las herramientas de Lean y Mathlib. Trabajaban en ramas de Git separadas, proponían cambios para integrarlos y utilizaban una base PostgreSQL compartida para reclamar tareas, compartir notas y registrar trabajo completado. Un evaluador comprobaba las pruebas enviadas.
Vuelvo a la misma idea: el estado compartido no hacía correcto el resultado por sí solo. Permitía trabajar en paralelo. El verificador de pruebas ofrecía una forma separada de evaluar los artefactos matemáticos producidos por ese trabajo.
Coordinar y verificar son tareas diferentes
Una base compartida puede indicar qué subproblema está disponible. Git conserva cambios y detecta conflictos. Ninguno demuestra automáticamente que una afirmación matemática se deduce de las hipótesis establecidas. Lean comprueba una prueba formal frente a sus definiciones y reglas; el valor del resultado también depende de qué expresan realmente esas definiciones e hipótesis.
Por eso evitaría traducir el titular directamente como «mil agentes pueden resolver cualquier problema difícil». El experimento tenía una estructura especialmente útil: los investigadores podían definir hitos, el trabajo formal previo aportaba lemas y existía un verificador concreto. Muchas tareas de software y negocio no definen con tanta claridad qué significa un resultado correcto.
La comparación del anuncio de Anthropic también es limitada. Su gráfico presenta una única ejecución por modelo en esa configuración. Una formalización más rápida en un experimento concreto no establece una mejora general de velocidad ni una garantía de fiabilidad para otros equipos, tareas o presupuestos.
El límite de seguridad fue diseñado
Anthropic describe una máquina virtual ligera por agente, sin acceso directo a la red desde esos entornos, y una pasarela para las peticiones de Git y de base de datos permitidas. Un clasificador en tiempo real examinaba las llamadas a herramientas, mientras otro monitor revisaba las acciones fuera de línea. La empresa afirma que ninguna acción de esta ejecución alcanzó su umbral de bloqueo.
Estos detalles importan porque los agentes paralelos aumentan el número de acciones que un sistema debe observar. Un monitor y un entorno aislado pueden reducir el riesgo, pero su presencia no demuestra que todas las fallas o escapes posibles sean imposibles. La pregunta útil es qué puede hacer el sistema, qué puede detener cada control y cómo puede una persona inspeccionar o intervenir.
Qué llevaría a un proyecto de ingeniería
Antes de añadir más agentes a un proyecto, haría explícita la señal de aceptación. ¿Qué evidencia muestra que una tarea está terminada? ¿Qué hipótesis quedan fuera del verificador? ¿Dónde vive el estado compartido y quién puede modificarlo?
Empezaría con trabajo divisible sin escrituras que se solapen. Mantendría visibles los artefactos y las decisiones. Daría a cada trabajador el acceso mínimo necesario. Después mediría si la coordinación, la verificación y la revisión siguen funcionando al aumentar el número de trabajadores.
Lo interesante del experimento no es solo el tamaño del equipo. Es la combinación de un problema acotado, contexto matemático proporcionado, coordinación compartida y una comprobación ejecutable. Son ingredientes más difíciles de resumir en un titular y mucho más útiles al diseñar un sistema de agentes.
Fuentes
- Anthropic: Claude Fable 5.2 y Mythos 5.2, 9 de noviembre de 2026.
- Claude.dev: escalar equipos multiagente con Claude Fable 5.2, 9 de noviembre de 2026.
- Lean: logotipo oficial y política de marcas. El logotipo de Lean sin modificar y su símbolo de marca identifican el asistente de pruebas; su uso no implica respaldo de Lean FRO.
Fuentes revisadas el 11 de noviembre de 2026. Sigue jpalanco.com para más notas sobre IA, ingeniería y herramientas de código abierto.
