MathCode: KI-Assistent beweist mathematische Sätze in Lean 4
MathCode, Mathematical Coding Agent
MathCode ist ein Terminal-basierter KI-Coding-Assistent mit integrierter Formalisierungs-Engine. Er übersetzt mathematische Probleme aus natürlicher Sprache in Lean-4-Theoreme und versucht, sie formal zu beweisen. Zu den Funktionen gehören eine persistente Lean-REPL, wiederverwendbare Theorem- und Axiom-Bibliotheken, agentenbasiertes Beweisen, parallele Beweisstrategien und ein Obsidian-Wissensgraph. Der Assistent benötigt macOS (arm64) oder Linux (x86_64) und die codex-CLI als Backend. Er reduziert die Kompilierzeit auf etwa 0,4 Sekunden und nutzt Lean-LSP-Integration, um verifizierte Mathlib-Lemmata zu finden.
Jeder bewiesene Satz wird automatisch benannt, gespeichert und importierbar gemacht, sodass der Beweiser und der Planer ihn wiederverwenden können.