3 ms·
Honestly I think no single system of writing is powerful enough to handle all the different versions of algebra. Mathematics can be extremely concise but only b
by contravariant 3y ago
Honestly I think no single system of writing is powerful enough to handle all the different versions of algebra. Mathematics can be extremely concise but only by constantly omitting stuff or overriding the meaning of symbols.
There are some happy accidents like df/dx making sense as both a derivative and a division of 1-forms, but on the whole you can't pick a single notation and hope for it to work well in all situations, yet that seems to be what most algebra systems do out of necessity.
To fix this I reckon we'll need to standardize not the automated algebra part but rather get those systems to communicate using some standardized format. Which is nigh impossible because of the sheer variety of mathematical concepts, but one can hope.
- viscousviolin 3y agoI don't think it's as difficult as you think it is. It's still a lot of work to implement mind you, but not nearly impossible. I talked about Mathlib [0] in a reply to the grandparent comment, which is a library of mathematical theorems and proofs that has a big community effort behind it. The language they use to state theorems would help a lot in making mathematics machine-readable enough for a computer algebra system to be able to make sense of it. I'm hoping to build a prototype for this sometime in Julia's `Symbolics.jl` CAS. It would be just a simple proof of concept to implement derivative and integral rules from Mathlib or some custom maths library, and get them into the CAS. Symbolics.jl seems to be a perfect fit for this since it's made to be extensible, and Julia's metaprogramming would be a welcome addition as well. Either way, I would love to see this become part of the CAS ecosystem. [0] https://leanprover-community.github.io/ https://leanprover-community.github.io/