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.
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.
You could add support also for the Woxi[1][2] for most of the symbolic math, also should be way faster than bunch of glue over different Python libraries.
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?
Consider the problem the above GitHub repository attempts to address:
That problem (which is absolutely huge if you think about it) is that at this point in time in Earth's history, at this point in time in Earth's AI evolution,
We cannot reliably do advanced mathematics on LLM's.
That is, we can ask LLM's to solve advanced mathematical problems for us by prompting them to.
But as to whether or not they output the correct answer is largely hit-or-miss.
They may output the correct answer, but then again, they may not.
If they output the correct answer, it's usually because someone, somewhere, on some web page,community, social media or discussion forum of the Internet posted text of the correct answer, and the LLM was trained on that text.
At no point is the LLM actually "thinking" about the work, showing steps, or comprehensively proving / disproving work at each step.
Thus when it arrives at an answer to an advanced math problem, the answer could be correct, but is never, with mathematically rigor, proven to be correct.
Correspondingly, there is always the risk that a query involving advanced math will be wrong.
The above GitHub repo attempts to fix that problem by transitioning the problem solving, associated proofs (and/or subgoals for proofs) to Python code / Python libraries / other libraries (i.e., NumPy, SymPy, numba, mpmath, CuPy, Z3, Lean, etc., etc.) to name a few.
The above GitHub repo attempts to fix that problem by generating an external MCP server employing the above, thus, all the LLM needs to do is call the implemented MCP server.
Heck, you might call it "Math As A (MCP) Service)" (a MaaS!), if it works!
Now some posters have commented that it looks AI Generated itself.
Yes, that's possible - that may have been necessary to create the initial GitHub repo and get it off the ground -- but the real question is, what is this thing going to be capable of in a year or more from now, once it has garnered some community support, once it has garnered some more human contributors?
It looks like it has the possibility to turn out (depending how it is implemented in the future!) pretty nifty!
I would be optimistic, cautiously optimistic, about this project going into the future!
It looks like (again, if properly implemented!) it could go a long way to solving the LLM's can't reliably do advanced math problem, which, at least at this point in time in the history of the evolution of AI on planet earth is a very real, very big problem!
So, from that perspective, I think that this project (and others like it!) will highly be worth watching in the future...
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.
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.
You could add support also for the Woxi[1][2] for most of the symbolic math, also should be way faster than bunch of glue over different Python libraries.
[1] https://woxi.ad-si.com/
[2] https://github.com/ad-si/Woxi
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?
Consider the problem the above GitHub repository attempts to address:
That problem (which is absolutely huge if you think about it) is that at this point in time in Earth's history, at this point in time in Earth's AI evolution,
We cannot reliably do advanced mathematics on LLM's.
That is, we can ask LLM's to solve advanced mathematical problems for us by prompting them to.
But as to whether or not they output the correct answer is largely hit-or-miss.
They may output the correct answer, but then again, they may not.
If they output the correct answer, it's usually because someone, somewhere, on some web page,community, social media or discussion forum of the Internet posted text of the correct answer, and the LLM was trained on that text.
At no point is the LLM actually "thinking" about the work, showing steps, or comprehensively proving / disproving work at each step.
Thus when it arrives at an answer to an advanced math problem, the answer could be correct, but is never, with mathematically rigor, proven to be correct.
Correspondingly, there is always the risk that a query involving advanced math will be wrong.
The above GitHub repo attempts to fix that problem by transitioning the problem solving, associated proofs (and/or subgoals for proofs) to Python code / Python libraries / other libraries (i.e., NumPy, SymPy, numba, mpmath, CuPy, Z3, Lean, etc., etc.) to name a few.
The above GitHub repo attempts to fix that problem by generating an external MCP server employing the above, thus, all the LLM needs to do is call the implemented MCP server.
Heck, you might call it "Math As A (MCP) Service)" (a MaaS!), if it works!
Now some posters have commented that it looks AI Generated itself.
Yes, that's possible - that may have been necessary to create the initial GitHub repo and get it off the ground -- but the real question is, what is this thing going to be capable of in a year or more from now, once it has garnered some community support, once it has garnered some more human contributors?
It looks like it has the possibility to turn out (depending how it is implemented in the future!) pretty nifty!
I would be optimistic, cautiously optimistic, about this project going into the future!
It looks like (again, if properly implemented!) it could go a long way to solving the LLM's can't reliably do advanced math problem, which, at least at this point in time in the history of the evolution of AI on planet earth is a very real, very big problem!
So, from that perspective, I think that this project (and others like it!) will highly be worth watching in the future...
[dead]
[flagged]