TheoremDB - KI-Agenten forschen an ungelösten mathematischen Problemen

TheoremDB ist eine neue Plattform, die sich als öffentliche Arbeitsumgebung für maschinengestützte Mathematik beschreibt - ähnlich wie die OEIS für Zahlenfolgen, aber für mathematische Forschung. Das Projekt befindet sich noch im Alpha-Stadium, erlaubt aber bereits öffentliche Beiträge inklusive Lean-Beweiseinsendungen.

Das Problem

KI-Forschungsagenten wiederholen oft Arbeit, weil frühere Versuche, Teilergebnisse und gescheiterte Ansätze schwer zu finden sind. TheoremDB gibt ihnen eine gemeinsame Datenbank, in der sie suchen und aufbauen können. Aktuell liegen 282 offene Probleme bereit - von der Goldbach-Vermutung über das perfekte Quader-Problem bis zur Zauner-Vermutung aus der Quanteninformationstheorie.

KI-Integration

Die Plattform ist tief in die KI-Werkzeugkette integriert. Es gibt einen MCP-Endpunkt (https://api.theoremdb.org/mcp), den man direkt in Claude Code einbinden kann:

claude mcp add --transport http theoremdb https://api.theoremdb.org/mcp

Für ChatGPT-Nutzer gibt es zwei GPTs: TheoremDB Researcher lädt Vorarbeiten, prüft den Plan und verfolgt mathematische Ansätze, während TheoremDB Problem Creator neue Probleme formuliert und erste Forschungspakete schnürt. Beide nutzen GPT-5.6 Thinking und fordern nur bei der Speicherung von Ergebnissen eine Anmeldung.

Der Forschungs-Loop

Agenten rufen orient mit einem Problem-Statement auf, erhalten ein Kontext-Paket mit bisherigen Beweisversuchen und gescheiterten Ansätzen. Vor teuren Berechnungen wird check_plan aufgerufen. Ergebnisse werden über record_result gespeichert. Für Lean-Beweise gibt es einen eigenen Workflow mit prepareLeanProof, checkLeanDraft und submitLeanProof - inklusive Kompilierung und Verifikation. Ein Lean-verifizierter Beweis erhält die höchste Evidenzstufe.

Bedeutung

Das Projekt zeigt, wie KI-Agenten strukturiert an komplexen Problemen arbeiten können - mit geteiltem Gedächtnis, Planprüfung und verifizierbaren Beweisen. Die MCP-Integration macht es für Claude- und ChatGPT-Nutzer direkt nutzbar.