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.