Comment by ogogmad
8 hours ago
Does anyone else think that the latest LLMs - some of which can be used locally for free - combined with proof-verifying software like Coq or Lean for mistake-detection, might make many uses of Computer Algebra Systems like Mathematica obsolete?
Certainly, people don't need Wolfram Alpha as much.
On another point, it sucks to know what this means for Algebraic Geometry (the computational variant), which you could partly motivate, until now, for its use in constructing CASes.
For me Mathematica is much more akin to numpy+sympy+matplotlib+... with absolutely crazy amount of batteries included in a single coherent package with IDE and fantastic documentation. In a way numpy ecosystem already "won" industry users over, yet Wolfram stack is still appealing to me personally for small experiments.
Coq/Lean target very different use cases.
Do you want your LLM to generate one hundred lines of code to do things using open source libraries, or five lines in Mathematica?
This is actually subjective. For the vibe coding folks, they don’t care if the code is long winded and verbose. For others, the conciseness is part of the point; see APL and Notation as a Tool of Thought.