Sounds like it’s mostly lisp. How mathematically correct and proven (in the math sense) is lisp?
This is just a backbone for array computations, at a lower level than numpy. It's more about JIT-compilation of a small handful of operations than math overall
It might be easier to write correct code in (emphasis on the might).
You could say lisp is more elegant though, as everything is an expression and the language is homoiconic.
There's degrees of truth to this. For example, most production lisps will compile functions to native code instead of storing the literal list of expressions. It's easy to manipulate lisp code before that happens but there's certainly a point where the homoiconicity is sacrificed.
Check out "The Definition of Standard ML" to get a sense of what a (mostly kosher) formal programming language definition might look like.