Google Uses Multiple Specialized AI Agents to Build Teamwork System, Successfully Verifies Multiple Complex Mathematical Proofs
IT之家 reported on November 14 that Google announced it is further expanding its Antigravity multi-agent system, using multiple specialized agents powered by Gemini models to form the Teamwork system, which it claims can solve “long-standing unsolved mathematical problems,” “verify complex mathematical proofs,” and optimize the performance of various software systems.
For example, Google has successfully formalized a proof of the Weil conjectures. This is a set of important mathematical results about the number of solutions to polynomial equations over finite fields, originally proved by mathematician Pierre Deligne (Pierre Deligne) in 1974. Google’s Teamwork-LEAP system completed the formalization of the related mathematical results through about 28,800 sub-agent calls, generating a cumulative total of about 1.8 million lines of Lean code.
Google also said the system recently successfully reproduced a formal proof of the finite-time blow-up problem for the three-dimensional Navier–Stokes equations, and helped researchers solve the Courtade–Kumar conjecture.

Technically, Google’s Teamwork system mainly relies on multiple agents working in parallel, and arranges independent systems to question and verify proposed solutions, in order to reduce errors that a single AI model may make when generating long reasoning processes. Each specialized agent can only access the files and tools