I spent a few days playing around with this work in Lean and his central claim is provably wrong..

The main problem is that singularities infect everything, and you can't have an equational theory without rewrite/substitution rules that aren't grounded unless you can decide if an arbitrary EML tree is zero, which is undecidable in elementary functions (because of sine).

Basically it's only valid on a undecideable subset. All of his numerical tests are carefully crafted to avoid singularities which are exactly where it fails, and the singularities are all over the place -- in particular in subtraction (which shouldn't have any!). He wants to sort of compile it to actually computable functions and use those instead, but there is no equational theory possible that you can build with this.

You can't restrict it to the positive reals either or it's not closed, it's trivially easy to get to complex or negative numbers.

Using extended reals doesn't fix it, you just get different undefined terms (-inf + inf = 0).

It's quite pretty! I love the idea or I wouldn't have spent so much time on it. It just doesn't work, and none of his other candidates will work either because they all have ln(0).

The only sense in which it's true which is that it can generate the elementary functions that it can generate, which is just tautological. It can in no sense generate all of them.

Even his verification doesn't work because they set it up to check the narrow bands where it's valid, outside of that it's a mess.