How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem.
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 codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel.
Fair enough, that would be nice. However, it sounds like a very hard thing to build in practice. I'd expect, actually, it's best done in Lean itself. So you're proposing a CAS written in Lean, which noone is currently working on.
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) automatically. All in all, proof assistants aren't computer algebra systems. You could make computer algebra systems in those frameworks but I'm not aware of any.
Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case.
This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations,
All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful.
Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.
Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations?
Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them)
TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.
In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms).
Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance)
If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.
A CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what math would be missing?
Comments
How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem.
[0] https://leanprover-community.github.io/
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 codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel.
[0] https://news.ycombinator.com/item?id=37435449
Fair enough, that would be nice. However, it sounds like a very hard thing to build in practice. I'd expect, actually, it's best done in Lean itself. So you're proposing a CAS written in Lean, which noone is currently working on.
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) automatically. All in all, proof assistants aren't computer algebra systems. You could make computer algebra systems in those frameworks but I'm not aware of any.
Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case.
This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations,
All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful.
How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_sc...
CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio...
Rewriting: https://en.wikipedia.org/wiki/Rewriting
Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance.
eBPF is not a rules engine, but it does optimize filter sets IIRC?
Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.
FWIU Wolfram's searching for a unified model with the Wolfram Physics Project, too; e.g. "The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics" (2022) https://www.wolframscience.com/metamathematics/ https://www.wolframphysics.org/bulletins/
Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations?
Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them)
TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.
I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... :
Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance)
If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.
Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.
A CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what math would be missing?