正文 · AI 翻译
IT Home reported on November 14 that Google announced a further expansion of its Antigravity multi-agent system. Its Teamwork system brings together multiple specialized agents powered by Gemini models and, Google 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. These are a set of important mathematical results concerning the number of solutions to polynomial equations over finite fields, originally proved by mathematician Pierre Deligne in 1974. Through approximately 28,800 sub-agent calls, Google's Teamwork-LEAP system generated a total of about 1.8 million lines of Lean code to formalize the relevant mathematical results.
Google also said that the system recently succeeded in reproducing a formal proof concerning the finite-time blow-up problem for the three-dimensional Navier–Stokes equations. It also helped researchers resolve the Courtade–Kumar conjecture.
Technically, Google's Teamwork system relies mainly on multiple agents working in parallel and assigns independent systems to challenge and verify proposed solutions, reducing errors that a single AI model might make while generating lengthy reasoning. Each specialized agent can access only the files and tools needed to complete its task. Independent challengers and reviewers then check the results without relying on the original agent's reasoning process.
Beyond mathematical research, Google has also applied the technology to molecular chemistry. A team of 30 specialized agents, working with a simulator that incorporates physical knowledge, uses nuclear magnetic resonance (NMR) data to identify molecular structures. On a benchmark of complex molecules, the system achieved Top-1 accuracy of 95% and Top-3 accuracy of 100%.
Google also demonstrated applications of multi-agent collaboration in systems engineering. The company said its team of agents rewrote its libgav1 AV1 video decoder from C++ in Rust, ultimately generating about 170,000 lines of code and producing output identical to the original version across a broad test suite.
Google is currently making the Teamwork system and an iterative programming workflow called /boost available to users through Antigravity. It plans to offer 10,000 academic researchers free access at the highest usage limit for 6 months.