Article

Star Fleet Math: Parallele GPT-5.6-Instanzen lösen 27 Erdős-Probleme

AI GPT-5 Mathematik Lean 4 Erdős Automated Theorem Proving

Ein neues AI-System namens Star Fleet Math hat sich vorgenommen, was unmöglich schien: die Lösung der härtesten offenen mathematischen Probleme der Welt. Mit einem parallelen Ansatz aus bis zu 20 GPT-5.6-Instanzen und formaler Verifikation in Lean 4 wurden bereits 27 Erdős-Probleme mit vorgeschlagenen Lösungen versehen.

Das System hinter Star Fleet

Star Fleet ist eine Mac-Desktop-App, die individuelle “Starship” genannte agentische Harnesses steuert. Jeder Starship läuft auf einem dedizierten 60-vCPU-Server und arbeitet autonom an einem separaten mathematischen Problem. Die Architektur kombiniert:

  • Massive Rechenpower: Bursts von bis zu 2.000 vCPUs für sharding-optimierte Suchprogramme
  • H100 GPU-Cluster für massiv parallele Suchläufe
  • Gemini-Embeddings-2 + Chroma Vektor-DB für die weltgrößte Lean 4 Theorem-Korpus-Suche in Plain English
  • Firecrawl.dev Index von arXiv-Papern und GitHub-Repos
  • Claude Fable API als Proof-Verifier im agentischen Harness

Besonders interessant: Das System nutzt Ton 618, ein lokales Langzeitgedächtnis, in dem jedes verifizierte Lean 4-Theorem in einen Abhängigkeitsgraphen gewoben wird – so “komponieren” sich die Beweise.

Die Ergebnisse

Von 650 getesteten Problemen (630 Erdős, 14 Frontier Math, 6 Millennium) wurden 27 als “Solution Proposed” markiert. Das Team betont dabei, dass sie sorgfältig Probleme vermieden haben, zu denen bereits inoffizielle Antworten online existierten.

Jede Lösung durchläuft einen strengen Überprüfungsprozess:

  1. Lean 4 formale Verifikation
  2. Claude Fable API Review
  3. Optional: Menschliche Review per iMessage

Technische Details

Die Starships greifen auf vorkonfigurierte Sandboxes zurück mit:

  • SAT/SMT-Solver (CaDiCaL, kissat, Z3)
  • Google CP-SAT
  • Computeralgebrasysteme (SageMath, PARI/GP, GAP, Macaulay2)
  • Rust, CUDA C++, Lean 4 Toolchains

Der gesamte Stack wurde in TypeScript & Bun from scratch entwickelt.

Was das bedeutet

Das Projekt zeigt, wie weit parallele Agentensysteme gekommen sind – und wie formale Verifikation mit LLMs kombiniert werden kann. Dass GPT-5.6 hier zum Einsatz kommt (ein Modell, das öffentlich noch nicht existiert), wirft interessante Fragen zur Entwicklung der Modell-Generationen auf.

Die vollständige Liste der gelösten Probleme und Download-Links für die Lösungen sind auf der Projektseite verfügbar.