KI, die Mathematik beweist, ist die heißeste Storyline des Jahres 2026 — Versuche zur Riemann-Vermutung, fallende Erdős-Probleme, OpenAI’s Astra. All das ist in Frontier Labs gesperrt. MathCode ist das Bauteil, das Sie tatsächlich installieren können.
Es ist ein Open-Source-Terminal-Agent von math-ai-org. Beschreiben Sie einen Satz in einfachem Englisch; er schreibt die Lean 4-Formulierung und erzeugt einen maschinell geprüften Beweis. Im Grunde Claude Code für Mathematik — 657 GitHub‑Stars, Titelseite von HN.
Warum es tatsächlich iterieren kann
Formale Beweise sterben meist an der Kompilierzeit: ~30 Sekunden pro Lean‑Check. MathCode hält ein persistentes Lean‑REPL warm und reduziert das auf ~0,4 Sekunden, sodass der Agent Hunderte Male versuchen, scheitern und erneut versuchen kann. Harte Theoreme werden über einen Tree-of-Subgoals aufgeteilt – Teilbeweise laufen parallel und werden dann zu einem Skelett zusammengefügt. Alles Bewiesene landet in einer wiederverwendbaren Theorem‑Bibliothek, abgebildet als Obsidian‑Abhängigkeits‑Graph.
Bringen Sie Ihr eigenes Modell
Es ist ein CLI mit austauschbaren Backends: Codex standardmäßig, plus Anthropic‑ und OpenRouter‑Schlüssel (DeepSeek, Gemini, Grok), erweiterbar durch Skills und Plugins. Der offensichtliche Anwendungsfall: Prüfen, ob ein „Proof“ eines LLM tatsächlich kompiliert. In KI‑Mathematik ist die Generierung billig – die Verifikation ist der Engpass, und genau das liefert dieses Tool.