Google says Gemini 4 agent teams solved open math problems and formalized the Weil conjectures

Google Research has published results from /teamwork, a multi-agent feature in its Antigravity coding environment that runs on Gemini 4 models, saying teams at Google and partner universities used it on open problems in mathematics, chemistry, systems software and machine learning engineering over the past several weeks, according to a blog post by Google Fellow Vahab Mirrokni. Google says all of the work was done with human experts.

Researchers from Google, CUHK, USC and CMU used /teamwork to prove information theory's 2013 Courtade-Kumar conjecture in full generality, Google says. A related framework, LEAP, built with Google Cloud AI, fully autonomously produced a machine-checked formalization of the Weil conjectures in the Lean proof language, about 1.8 million lines across 28,800 subagent invocations. Google says it also produced first formalizations of the Birkhoff conjecture, open since 1927, and of the 3D Bochner-Riesz conjecture, where it found and fixed a gap in a recently released informal proof.

The system pairs parallel agents with checkers such as the Lean 4 proof checker, unmodified test suites and simulators, and gives each agent only the files and tools it needs for one step. Other results Google reports include about 800,000 lines of Rust written to finish porting the Zircon microkernel and a 24% reduction in TPU workload preemption on some hardware types in its Borg scheduler.

Google says external scientists and developers can use Gemini 4 models with /teamwork in Antigravity today, and it has opened applications for 10,000 academic researchers to get six months of free access to its highest usage tier.