MathKernel: An evidence-aware multi-engine mathematics kernel and MCP server

I'm building a project in this area called Alkahest: https://github.com/alkahest-cas/alkahest. It is a computer algebra system built in Rust that emits corresponding Lean certificates for many of its operations that can be formally verified.

Alkahest is available as a Python library or a Rust crate. It's designed for agent use with good debugging output.

I'm rapidly iterating on it, feel free to send any issues/comments/ideas my way.

As a side note, the name "MathKernel" is overloaded -- that's what Mathematica's own kernel executable is called, which is a little unfortunate when you have tooling that already refers to it.

Though it has all the signs of being AI-generated, this looks like a pretty interesting project. But by itself, it seems sort of like a game engine without a game. Have you done something interesting with it?

[flagged]