MathKernel: Ein Mathematik-Kernel für LLMs mit Beweisprotokollen
MathKernel: An evidence-aware multi-engine mathematics kernel and MCP server
MathKernel ist eine Open-Source-Python-Bibliothek und ein MCP-Server, die Large Language Models von der Arithmetik entlasten: Das LLM interpretiert die Absicht, der Kernel rechnet und dokumentiert für jedes Ergebnis einen Vertrauensgrad, die verwendete Engine und eine Herleitungsspur. Exakte Arithmetik, symbolische Resultate, zertifizierte Intervalle, empirische Evidenz und formale Beweise werden klar unterschieden. Unterstützt werden unter anderem symbolische Algebra, Graphentheorie, Statistik, PDEs und formale Verifikation mit Lean.
Das LLM interpretiert die Absicht; der MathKernel etabliert mathematische Evidenz.
- nxobject
Nebenbei bemerkt ist der Name "MathKernel" mehrdeutig – so heißt nämlich auch die eigene Kernel-Datei von Mathematica, was etwas unglücklich ist, wenn man bereits Tools hat, die sich darauf beziehen.
- overfitCNN
Ich baue ein Projekt in diesem Bereich namens Alkahest: https://github.com/alkahest-cas/alkahest. Es ist ein Computeralgebrasystem in Rust, das für viele seiner Operationen entsprechende Lean-Zertifikate ausgibt, die formal verifiziert werden können.
Alkahest ist als Python-Bibliothek oder Rust-Crate verfügbar. Es ist für den Einsatz durch Agenten konzipiert und bietet gute Debug-Ausgaben.
Ich entwickle es schnell weiter; schickt mir gerne Probleme, Kommentare oder Ideen.
- xvilka
Du könntest auch Unterstützung für Woxi[1][2] für den Großteil der symbolischen Mathematik hinzufügen; das sollte auch viel schneller sein als ein Haufen Kleber über verschiedene Python-Bibliotheken.