Things I would like to see in a computer algebra system
&gt; Pretty much the only systems that more or less get math right are the mathematical libraries for proof assistants (Lean, Coq, etc.). The mathematical structures and interfaces in Lean&#x27;s MathLib are actually pretty close to what I&#x27;d like to see in a CAS.<p>This comes with HUGE practical disadvantages. Yes, it would be possible to use type theory to make a mathematically rigorous CAS, but it would never be practical. Anyone who has ever tried knows that even proving something trivial like a+b+c+d=d+b+c+a in a theorem prover requires a suprising amount of ingenuity. There are few people in the world who have the skills to define and prove something more advanced like Buchberger&#x27;s algorithm, and a task like that would probably require several math papers worth of new research just to produce the slowest implementation known to mankind. And it would take years.