MathKernel kobler fem regnemotorer til MCP og merker hvert svar med tillitsnivå

Fem klasser av regnemotorer, sympy, z3, lean, numba og cuda, ligger bak MathKernel, et prosjekt som kan brukes både som Python-bibliotek og som MCP-server under navnet mathkernel-mcp. Det kjører på Python 3.11 eller nyere, er lisensiert under MIT, og README-en oppgir versjon 1.3.0.

Arbeidsdelingen er hele poenget.

«Språkmodellen tolker intensjonen, MathKernel etablerer det matematiske beviset.» Slik oppsummerer prosjektet sin egen premiss: modeller er gode på matematisk hensikt og dårlige på matematisk aritmetikk.

Dette er noe annet enn nok en kalkulator bak et verktøykall, fordi hvert resultat bærer tre ting: et tillitsnivå, en merkelapp for hvilken motor som produserte det, og et derivasjonsspor. Prosjektet skiller eksplisitt mellom eksakt beregning, symbolske resultater, sertifiserte innhegninger med intervallaritmetikk, empirisk evidens og formelle bevis kontrollert av Lean-kjernen. Det er distinkte påstander, ikke gradsforskjeller av samme sak.

MathKernel er strengest der slike systemer vanligvis er slappest, nemlig i overgangene. README-en slår fast at eksakt aritmetikk alene ikke er et formelt bevis, og at opphavet til et tilnærmet inndata ikke får forsvinne stille underveis i en utregning. Et resultat som stammer fra flyttall, kan altså ikke ende opp merket som eksakt lenger nede i kjeden. Prosjektet er like tydelig på at enighet mellom flere motorer ikke i seg selv er et bevis, og at én tillitsmerkelapp ikke erstatter selve evidensbunten.

Arkitekturen er lagt opp som et typet orkestreringslag i stedet for én stor løser. En fasade eier parsing, kontekster, objektidentitet, persistens, ressurspolicy og derivasjonssporing, mens domeneadaptere gjør selve matematikken. Presentasjonslagene, blant dem visualisering og sonifisering, ligger nedstrøms og kan etter designet ikke gjøre en påstand sterkere enn den var. Et pent plott gir ingen ny evidens.

Funksjonsmatrisen dekker svært mye, fra symbolsk algebra og kompleks analyse til eksakte grafalgoritmer, endelig algebra, PDE-er med adaptive elementmetoder og informasjonsgeometri. Bredden er også grunnen til å være litt avventende: hver rad i matrisen oppgir sitt eget evidenstak, og det er en betydelig mengde påstander å innfri for ett prosjekt. Verdien for deg ligger uansett mindre i dekningen enn i at et verktøykall fra en agent kommer tilbake med en merkelapp du kan avvise på.

Hva bør du gjøre?

1. Koble mathkernel-mcp på som MCP-server hvis agenten din regner på noe som får konsekvenser. Da får du et svar med tillitsnivå i stedet for et tall uten opphav.

1. Behandle tillitsnivået som et filter i din egen kode. Et resultat merket NUMERIC eller EMPIRICAL bør ikke gå videre samme vei som et FORMAL-resultat.
2. Sjekk derivasjonssporet på et par kjente utregninger før du stoler på flaten. Det er den raskeste måten å se om merkelappene faktisk oppfører seg som README-en beskriver.