Googles KI-Agententeams knacken jahrzehntealte Mathe-Probleme und schreiben Kernel in Rust

Worum es geht

Google Research hat am 13. November 2026 einen langen Bericht über neue Ergebnisse von /teamwork veröffentlicht. Das ist eine Funktion in Antigravity, Googles KI-gestützter Entwicklungsumgebung. Darin arbeitet nicht ein einzelnes Sprachmodell, sondern ein ganzes Team von KI-Agenten zusammen: Programme, die selbstständig Teilaufgaben erledigen, Werkzeuge bedienen und sich gegenseitig kontrollieren. Den Beitrag hat Vahab Mirrokni geschrieben, Google Fellow und Vizepräsident bei Google Research. Er ist auf dem Google-Research-Blog nachzulesen.

In den vergangenen Wochen haben Teams bei Google und an Partneruniversitäten mit den neuen Modellen Gemini 4 Argon, Gemini 4 Carbon und Gemini 4 Hydrogen an Problemen gearbeitet, die teils seit Jahrzehnten offen waren. Dazu gehören Fragen aus Mathematik, theoretischer Informatik und Chemie, aber auch Softwareprojekte bei Google. Google betont, dass alle Arbeiten gemeinsam mit menschlichen Fachleuten entstanden sind. Die Werkzeuge stellt das Unternehmen auch Außenstehenden zur Verfügung: /teamwork, der kleinere Bruder /boost und das Prüfwerkzeug Deep Review lassen sich laut Google schon heute in Antigravity nutzen.

Antigravity selbst ist eine Programmierumgebung von Google DeepMind. Laut einem Einsteiger-Überblick von Geeky Gadgets gehören dazu ein „Agent Manager“, der KI-Agenten anlegt und verwaltet, ein Code-Editor mit KI-Hilfe und Browser-Tests direkt in Chrome. Mehrere Agenten können dort parallel an verschiedenen Teilen eines Projekts arbeiten.

Wie /teamwork funktioniert

Google begründet den Aufbau mit zwei Schwächen heutiger Sprachmodelle. Erstens sind ihre Antworten unberechenbar: Ein einzelner Versuch liefert selten sofort die richtige Lösung. /teamwork lässt deshalb viele Lösungsansätze parallel erkunden und schickt jeden durch einen Falsifizierer, also ein Werkzeug, das objektiv prüft, ob etwas stimmt. Das kann der Beweisprüfer Lean 4 sein, eine unveränderte Test-Suite, ein Simulator, eine Websuche oder ein Hardware-Zähler.

Zweitens verlieren Modelle bei mehrtägigen Aufgaben den Überblick, weil sich ihre Aufmerksamkeit über ein immer größeres Kontextfenster verteilt, also die Textmenge, die ein Modell gleichzeitig im Blick hat. /teamwork teilt den Kontext darum von vornherein auf: Jeder spezialisierte Agent bekommt nur die Dateien und Werkzeuge, die er für seinen Schritt braucht. Koordinatoren übergeben Aufgaben an „frische“ Nachfolger. Kritiker und Prüfer bewerten die Ergebnisse, ohne die Gedankengänge des ursprünglichen Agenten zu kennen. So sollen sie unvoreingenommen bleiben.

Die Arbeitsabläufe sind als Muster in natürlicher Sprache beschrieben, die sich selbst verbessern. /teamwork wählt für jede Eingabe das passende Muster aus. Es gibt Muster für verteiltes Programmieren, für lange Beweise und für die Prüfung von Dokumenten. /boost ist eine eigenständige Schleife aus Lösen und Prüfen für den Programmieralltag. Laut Google hat eine lange /teamwork-Kampagne alte Durchläufe ausgewertet und herausgefunden, dass eng verflochtener Code besser nacheinander als parallel bearbeitet wird. Damit wurde /boost verbessert, ein System hat also ein anderes optimiert.

Wie das im Detail aussieht, zeigt ein Bericht von 36Kr über eine frühere /teamwork-Veröffentlichung vom 27. August. Der „Long Proof“-Modus läuft demnach als Turnier: Für jeden Lösungsansatz gibt es einen „Advocatus Diaboli“, dessen einzige Aufgabe es ist, ihn zu widerlegen. Verworfene Wege werden mit den Einwänden aufbewahrt, und typische Fehler landen in einem gemeinsamen „Fallen-Register“. Schon damals reproduzierte das kleine Modell Gemini 3.7 Flash im Team drei Forschungsergebnisse, die Gemini 3.1 Pro zuerst erzielt hatte. 36Kr ordnet aber auch ein: Beim viel beachteten Knuth-Zyklen-Problem hatten andere KI-Modelle (Claude Opus 4.6, GPT-5.4 Pro) die Lösung schon im Frühjahr gefunden. Googles Beitrag waren dort elegantere Konstruktionen und formal geprüfte Beweise, kein Durchbruch aus dem Nichts.

Ergebnisse in Mathematik und Informatik

Das bekannteste neue Ergebnis ist der vollständige Beweis der Courtade–Kumar-Vermutung von 2013. Sie besagt: Wenn eine zufällige Bitfolge durch einen verrauschten Kanal geschickt wird, bewahrt keine Verdichtung der Eingabe auf ein einzelnes Bit mehr Information als eine „Diktatorfunktion“, die einfach ein einzelnes Eingabebit kopiert. Gemini fand zuerst Gegenbeispiele zu einer verallgemeinerten Vermutung des CUHK-Teams. Die Forschenden reduzierten das Problem dann auf eine Optimierung mit 14 Variablen. Gemini 4 Argon und ältere Gemini-Modelle lieferten den Großteil der neuen Abschätzungen und Zertifikate mit Intervallarithmetik, einer Rechenmethode, die Rundungsfehler mathematisch sicher eingrenzt. Die Erweiterung auf unbalancierte Funktionen gelang laut Google ohne menschliches Zutun. Der gesamte Beweis wurde in Lean 4 formalisiert, einer Programmiersprache, in der ein Computer jeden Beweisschritt Zeile für Zeile prüft. Das Ergebnis umfasst 50 Millionen Codezeilen.

Weitere Ergebnisse laut Google:

• Adaptive Datenanalyse: nahezu optimale Schranken für statistische Abfragen, die auf frühere Antworten reagieren. Die Lücke war seit 2014 offen.
• Quantencomputing: erstmals n-Bit-Boolesche Funktionen, die mehr als n/2 Quantenabfragen benötigen (offen seit 2014).
• Boolesche Matrixmultiplikation: ein deterministischer Algorithmus, der die zentrale offene Frage der Konferenz STOC 2024 beantwortet.
• Ganzzahlmultiplikation: ein neuer O(n log n)-Algorithmus, dessen C-Umsetzung bis zu einer Milliarde Bits bitgenau mit der Bibliothek GMP übereinstimmt.
• Tarjans Deque-Vermutung von 1985: eine neue obere Schranke für Splay-Bäume, also sich selbst umsortierende Suchbäume, in Lean 4 geprüft.
• Dazu kommen Ergebnisse zu sparsamen Netzwerken, Matrixkompression, Streaming-Algorithmen für Graphen, Online-Optimierung und Kreuzvalidierung in der Statistik.

Die Autorinnen und Autoren haben die gelieferten Beweise laut Google geprüft, vereinfacht und für die Veröffentlichung überarbeitet.

Maschinell geprüfte Großbeweise

Das Agentensystem LEAP, entwickelt mit Google Cloud AI, übersetzt bereits vorliegende, informell aufgeschriebene Beweise in Lean. Nach Googles Angaben hat es die Weil-Vermutungen vollständig selbstständig formalisiert. Pierre Deligne hatte sie 1974 abschließend bewiesen. Die Formalisierung umfasst rund 1,8 Millionen Zeilen Lean aus 28.800 Aufrufen von Unteragenten. Hinzu kommen:

Wichtig: Hier hat die KI meist von Menschen gefundene Beweise maschinell überprüfbar gemacht und diese Probleme nicht selbst gelöst. Laut Google schließt eine Formalisierung versteckte Fehler aus, sobald Menschen bestätigt haben, dass die formale Aussage dem ursprünglichen Problem entspricht.

Außerdem bot Google vor der Konferenz STOC 2027 Deep Review an, ein Werkzeug, das Manuskripte auf Fehler prüft. Die Autoren von 578 Einreichungen nutzten es, mehr als ein Drittel aller Einreichungen. In einer noch laufenden Umfrage mit 70 Teilnehmenden hielten 90 Prozent das Feedback für überwiegend sachlich richtig. Über 30 Prozent gaben an, dass echte Beweisfehler gefunden wurden. Nutzer erhalten zwei kostenlose Deep-Review-Aufrufe pro Woche.

Chemie, Benchmarks und Software

In der Chemie arbeiteten 30 Agenten mit einem physikbasierten Spektrensimulator daran, Molekülstrukturen aus Messdaten der Kernspinresonanz (NMR) zu bestimmen. Dabei erreichten sie 95 Prozent exakte Treffer beim ersten Vorschlag und 100 Prozent unter den ersten drei, fast doppelt so viel wie ein einzelner Agent. 29 Agenten bauten in 11,5 Stunden aus 13 öffentlichen Tabellen einen Benchmark mit 50 Aufgaben zur kausalen Inferenz.

In der Software-Entwicklung fallen die Zahlen besonders auf. Ein neues Umschreib-Muster, das bald in Antigravity kommen soll, plant jedes Modul erst ein, wenn seine Abhängigkeiten kompilieren, und prüft es gegen die unveränderte Original-Test-Suite. So soll verhindert werden, dass Agenten Tests manipulieren. Auf diese Weise entstanden in zwei Wochen etwa 800.000 Zeilen sicheres Rust für den Zircon-Mikrokernel. Der Code besteht alle Kernel-Unit-Tests und bootet auf arm64-Hardware. Der AV1-Decoder libgav1 wurde in rund 170.000 Zeilen Rust neu geschrieben, mit 100 Prozent bitgenauer Übereinstimmung. Zunächst war die Rust-Version etwa viermal langsamer. Nachdem die Agenten Profiling-Werkzeuge bekamen, also Messprogramme für Rechenzeit, war sie 20 bis 30 Prozent schneller als das C++-Original samt handoptimiertem Assembler.

Weitere Beispiele: Eine Go-Engine für das 9x9-Brett gewann in unter acht Tagen rund 2.600 Elo-Punkte und erreichte 1.885 Elo. Beim Optimieren von TPU-Kernels, also Rechenroutinen für Googles KI-Chips, erzielte das Muster DuoDiscover eine durchschnittliche Beschleunigung um das 4,09-Fache über 17 Kernels. Intern fand /teamwork Speichereinsparungen von mehr als 1 PiB in Googles Rechenzentren und senkte im Cluster-Verwaltungssystem Borg die Unterbrechungen von TPU-Jobs auf manchen Hardwaretypen um 24 Prozent.

Verfügbarkeit

Gemini 4 mit /teamwork, /boost und Deep Review ist laut Google ab sofort in Antigravity nutzbar. Laut 36Kr wird der Modus über den Befehl /teamwork-preview gestartet. Google hat Bewerbungen geöffnet, über die 10.000 Forschende sechs Monate lang kostenlos die höchste Nutzungsstufe erhalten. Das Muster für formale Beweise und weitere Spezialabläufe sollen in den kommenden Wochen folgen, zusammen mit ausführlichen Tutorials. Preise für den normalen Betrieb nennt der Beitrag nicht.

Einordnung

Die Ergebnisse sind breit und bemerkenswert, aber zum großen Teil Herstellerangaben. Die Mathe-Ergebnisse sollen als Paper erscheinen, ihre Prüfung durch Fachkollegen steht oft noch aus. Lean-Formalisierungen sind dabei ein starkes Argument, weil der Computer jeden Schritt kontrolliert. Das gilt aber nur, wenn die formale Aussage wirklich dem Problem entspricht. Bei Formalisierungen wie den Weil-Vermutungen oder Navier–Stokes hat die KI bekannte Beweise nachgebaut und keine neuen gefunden. Auch das Beispiel des Knuth-Problems zeigt laut 36Kr, dass „gelöst“ manchmal „eleganter neu bewiesen“ heißt.

Der eigentliche Kern ist methodisch: Fortschritt entsteht hier weniger durch ein größeres Modell als durch die Organisation. Viele Agenten mit getrenntem Kontext, harte automatische Prüfer und unabhängige Kritiker arbeiten zusammen. Ähnliche Ansätze verfolgen auch OpenAI und Anthropic. Google stellt die Werkzeuge allerdings direkt in ein öffentlich nutzbares Produkt. Offen bleibt, wie viel Rechenleistung solche mehrtägigen Kampagnen verschlingen und was sie Außenstehende kosten. Ebenso offen ist, wie gut sie ohne Googles interne Experten funktionieren.