Re:Towards a New SymPy
by Tachyooon on Friday September 08, 2023 @12:47PM
(#37436057)
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.
Re:Towards a New SymPy
by staunton on Friday September 08, 2023 @02:50PM
(#37437751)
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.
[0] https://news.ycombinator.com/item?id=37435449