MathCode: Ein mathematischer Coding-Agent mit Lean-4-Formalisierung

MathCode ist ein Terminal-basierter KI-Coding-Assistent, der mathematische Probleme formalisiert und mit Lean 4 beweist. Statt selbst Lean-Code zu schreiben, gibst du ein Problem in einfachem Englisch ein, und es generiert ein Theorem und versucht einen Beweis, mit einer persistenten REPL und einer Bibliothek wiederverwendbarer Theoreme.

Hauptfunktionen

• Persistente Lean-REPL: Nach einem einmaligen Aufwärmen sinken die Kompilierzeiten auf ~0,4s (von ~30s).
• Theorem-Bibliothek: Jedes bewiesene Theorem wird automatisch benannt, gespeichert und zur Wiederverwendung importierbar.
• Axiom-Bibliothek: Speichere Konversationsannahmen als persistente, kompilierte Lean-Deklarationen.
• Lean-LSP-Integration: Durchsucht leansearch.net und Loogle nach verifizierten Mathlib-Lemmata, nutzt strukturierte LSP-Diagnosen für Reparaturen.
• Obsidian-Theorem-Graph: Erzeugt einen visuellen Abhängigkeitsgraphen von Theoremen und Lemmata in Obsidian.
• Agenten-Modus: Interaktive Sitzungen, in denen der Agent Beweiskandidaten basierend auf Fehlern iteriert.
• Baum der Teilziele: Zerlegt komplexe Theoreme in unabhängige Teilziele, beweist sie parallel und fügt sie zusammen.
• Multi-Planner: Führt mehrere Planer parallel für verschiedene Beweisstrategien aus; der Beweiser wählt den besten Ansatz.

Schnellstart

Erfordert macOS (arm64) oder Linux (x86_64) sowie die codex-CLI für das Standard-Backend.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login

Teste es mit:

mathcode -p "beweise, dass das Quadrat einer geraden Zahl gerade ist"

Die Ausgaben werden in LeanFormalizations/ geschrieben. Eine Browser-Oberfläche ist über ./run webui verfügbar.

Dieses Tool richtet sich an Mathematiker, Forscher und Entwickler, die mit formaler Verifikation oder KI-gestütztem Theorem-Beweis arbeiten.