Thanks. That was a mess. Don't know what happened, but I fixed it this morning.

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.

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.

I believe this is correct: x/x = 1 everywhere except 0, where it has a removable singularity. So you can extend x/x holomorphically to full C.

This is completely different from the phenomenon described in the article: arccosh discontinuity can’t be dealt the same way. In fact complex analysis prefers to deal with it my making functions path-dependent (multi-valued).

Simple rule to keep in mind that even math savvy people seem to forget about is that: sqrt(x²) = |x| with bars for absolute value.

For a programmer, it's clear that we have lost the sign information but not the magnitude.

Simple. Makes most sign and solution reasoning explicit instead of implicit when solving quadratics or otherwise working with square roots.

While some comments do point out the general opaqueness of Mathematica, the goal of Simplify is actually documented in Mathematica and something which can be changed: https://reference.wolfram.com/language/ref/ComplexityFunctio...

The default is a balance between leaf count and number of digits. But the documentation page above gives an example of how to nudge the cost function away from specialised functions.

In this case, a heuristic like "less parameters, less operators and less function calls" covers all the cases.

I think "simplify" is pretty clear here. For trigonometric functions you would expect a trig function and an inverse trig function to be simplified. We all know what we'd expect if we saw sin(arcsin(x)) (ie x). If we saw cos(arcsin(x)) I'll spoil it for you: it simplifies to sqrt(1-x^2).

Hyperbolic functions aren't used as much but the same principle applies. Here the core identity is cosh^2(x) = sinh^2(x) = 1 so:

      sinh(arccosh(x))
    = sqrt(1 + cosh^2(arccosh(x))
    = sqrt(1 + x^2)

For Simplify, I expect its a black, or at least gray box to Mathematica maintainers, too.

It will have simple rules such as constant folding, “replace x - x by zero”, “replace zero times something with the conditions under which ‘something’ has a value”, etc, lots of more complex but still easy to understand rules with conditionals such as “√x² = |x| if x is real”, and some weird logic that decides the order in which to try simplification rules.

There’s an analogy with compilers. In LLVM, most optimization passes are easy to understand, but if you look at the set of default optimization passes, there’s no clear reason for why it looks like it looks, other than “in our tests, that’s what performed best in a reasonable time frame”.

That blackbox being their entire moat, I would assume they'd never want to open-source any function. Mathematica as a front-end has innumerable frustrating bugs, but its CAS is top-notch. Especially combined with something like Rubi for integration, for me nothing comes close to Mathematica for algebraic computations.

I think you would get sqrt(x^2) = x, if x belonged to the natural domain of sqrt, which is a Riemann surface, that may also be defined using the language of "sheaves". I don't know how to connect this to the article or Mathematica.

That's not what it simplifies to using a real or complex number domains for x, it's abs(x). CAS need type inference assumptions and/or type qualifiers to be more powerful.

Edit: Fixed stuff.