31–40 of 72 posts
The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…
Earlier quoted context omitted.
That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).
In Coq, the tactics system supports writing solvers than can both find a result and give you the proof that it's correct. If Lean also has a similar tactics system, then solvers could be written in that.
Earlier quoted context omitted.
That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).
That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS cod…
I’ve tried to appreciate SymPy but I always find myself running home to Mathematica. There’s simply no comparison. SymPy is like a match and Mathematica has the power of a sizeable thermonuclear warhead.
Earlier quoted context omitted.
In Coq, the tactics system supports writing solvers than can both find a result and give you the proof that it's correct. If Lean also has a similar tactics system, then solvers could be written in that.
Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that's not what a CAS is). (I doubt there is one in Coq that will do this, although I'm not sure). A symbolic algebra system is expected to do this simplification (and much more advanced ones) automati…
This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
I’ve tried to appreciate SymPy but I always find myself running home to Mathematica. There’s simply no comparison. SymPy is like a match and Mathematica has the power of a sizeable thermonuclear warhead.
It's true. Unfortunately Mathematica simply can't be used in many domains. I would really like to integrate mathematica with a type checker for automatic theorem proving. I think it could greatly alleviate the clunkiness of dependent types.
Earlier quoted context omitted.
It's true. Unfortunately Mathematica simply can't be used in many domains. I would really like to integrate mathematica with a type checker for automatic theorem proving. I think it could greatly alleviate the clunkiness of dependent types.
Do you know of attempts to integrate SymPy in this way?
The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…
Is there an existing CAS built on top of a SAT or SMT solver?