Weirdly enough, mathematicians have been manipulating expressions and writing proofs for centuries without (routinely) stumbling into contradictions all without the need of formal proof calculi or s-expressions.

I have nothing but admiration for projects like Lean and Coq and working in them can be a lot of fun (coupled with a lot of frustration when "obvious" things sometimes take an inordinate amount of time to prove), but Wiles' proof of FLT (the corrected version) was published in 1995. We're almost 30 years later and people are just now working on a formalisation which could take many years (https://leanprover-community.github.io/blog/posts/FLT-announ...). Mathematicians can't afford to be waiting for proof systems to catch up, at least not right now.

It wasn't until the 1930s that people realised second order logic with arithmetic will always lead to contradictions without guardrails. Before then all mathematics was done in the object language of whatever the field in question was and only translated to the meta language for succinctness after the fact.

The magic of modern maths is that we can now work only with the meta language and get results free from contradiction. For this we absolutely need a modern notation to do the new type of maths since we are no longer grounded by the reality of the object language.