Agentes de IA de Google verifican demostraciones matemáticas célebres y reescriben software completo: así funciona /teamwork

¿Qué es /teamwork?

Antigravity es el entorno de desarrollo con agentes de IA de Google. Su función /teamwork divide un problema complejo entre muchos "subagentes", es decir, instancias del modelo que se reparten tareas, proponen soluciones y se corrigen entre sí. El modelo principal usado en los experimentos fue Gemini 4 Argon, según el blog firmado por Vahab Mirrokni, vicepresidente de Google Research.

La clave del método está en los llamados "falsificadores": herramientas externas que comprueban de manera objetiva si una respuesta es correcta. En matemáticas, el principal es Lean 4, un asistente de demostraciones que revisa cada paso lógico de una prueba escrita en un lenguaje formal, de modo que un error no puede pasar inadvertido. En programación, se usan baterías de pruebas sin modificar y simuladores de ejecución.

Matemáticas verificadas por máquina

El resultado más llamativo es la formalización de las conjeturas de Weil, un pilar de la geometría algebraica cuya demostración completó el matemático Pierre Deligne en 1974. De acuerdo con Google, el sistema produjo de forma autónoma cerca de 1,8 millones de líneas de código Lean, tras unas 28.800 invocaciones de subagentes, y obtuvo una versión que el computador puede comprobar paso a paso.

La compañía también reportó más de 919.000 líneas de Lean para formalizar una demostración reciente relacionada con el décimo problema de Hilbert. Además, señaló que el sistema reprodujo de manera independiente la formalización de una prueba reciente sobre la formación de singularidades en las ecuaciones de Navier-Stokes en tres dimensiones con fuerzas externas suaves. Esto no equivale a resolver el problema del milenio asociado a esas ecuaciones, que sigue abierto.

En paralelo, investigadores de Google, la Universidad China de Hong Kong (CUHK), la Universidad del Sur de California (USC) y la Universidad Carnegie Mellon (CMU) publicaron en el repositorio arXiv un preprint titulado "A Proof of the Most Informative Boolean Function Conjecture". El trabajo presenta una demostración asistida por computador de la conjetura de Courtade-Kumar, planteada en 2013 en teoría de la información, y afirma que la prueba completa fue verificada en Lean. Al tratarse de un preprint, aún no ha pasado por revisión de pares. El propio artículo menciona que otros grupos obtuvieron demostraciones independientes de forma simultánea.

Software reescrito y más eficiente

En ingeniería de software, Google afirma que los agentes tradujeron al lenguaje Rust, considerado más seguro frente a errores de memoria, unas 800.000 líneas del microkernel Zircon en cerca de dos semanas. El sistema resultante superó las pruebas unitarias y arrancó en procesadores arm64. También reescribió en Rust el decodificador de video AV1 libgav1, con unas 170.000 líneas que reproducen bit a bit los resultados del original. Tras ajustes de rendimiento, quedó entre 20% y 30% más rápido que la versión en C++ y ensamblador optimizado.

En química, 30 agentes acompañados de un simulador espectral identificaron moléculas complejas a partir de datos de resonancia magnética nuclear (RMN) con 95% de acierto en el primer intento, casi el doble que un solo agente, según la empresa.

Acceso para investigadores

Google anunció que científicos y desarrolladores externos ya pueden usar los modelos Gemini 4 con /teamwork en Antigravity. Además, abrió convocatoria para que 10.000 investigadores académicos reciban seis meses de acceso gratuito a su nivel de uso más alto, mediante un formulario en línea. La compañía no publicó criterios de selección ni fecha de cierre, ni precisó si el programa tiene restricciones por país.

Varias funciones, como el método de demostración formal, figuran como "próximas" y aún no están disponibles para el público.

Preguntas y respuestas de contexto

¿Qué es /teamwork y cómo funciona?

Es una función de la plataforma Antigravity de Google que permite a decenas de agentes de IA, basados en Gemini 4, trabajar en equipo para resolver problemas complejos. El sistema divide las tareas entre subagentes que proponen soluciones y se corrigen mutuamente mediante herramientas externas que verifican la validez de los resultados.

¿Cuáles fueron los principales logros en matemáticas y programación?

El sistema logró verificar formalmente demostraciones matemáticas complejas, como las conjeturas de Weil, y tradujo con éxito cientos de miles de líneas de código al lenguaje Rust, mejorando la seguridad y el rendimiento del software.

¿Quiénes pueden acceder a esta tecnología actualmente?

Google abrió una convocatoria para que 10.000 investigadores académicos obtengan seis meses de acceso gratuito a través de un formulario en línea. Aunque los desarrolladores externos ya pueden usar Gemini 4 con /teamwork, algunas funciones avanzadas de demostración formal aún no están disponibles para el público general.