If you want to write mathematics for computers, you can use Coq, Lean, etc. - or, in a different direction, Mathematica.
I beg to differ. A lot of mathematics is written in LaTeX which is written for computers to render into traditional notation. No one uses LaTeX directly because it has a horrific syntax, but it doesn't have to be that way. There is no reason why one could not invent a notation that didn't require complex rendering. Programming languages are an existence proof.
Except, you know, proofs that are automatically checked by a proof system.
It's really hard to take a suggestion like "mathematical notation should be replaced by s-expressions" seriously. There's approximately 0% of working mathematicians who would think that this is a good idea (hell, not even most programmers think it's a good idea to write everything in s-expressions).
BTW, you might want to look up the work of Steven Wolfram and Gregory Chaitin. They both thought using s-expressions was a good idea, and they got quite a bit of mileage out of it.
This argument would make sense if nobody had ever come up with an alternative system of maths notation, but MathML, Mathematica, Coq, Isabelle, Lean, and many others exist, and yes, probably even some notation based on s-expressions (you could do mathematics in Pie[0], although it's probably not super pleasant since it's a toy language). They get their use for specific situations, as I mentioned before, but they haven't replaced mathematical notation wholesale.
(And note too that even with a heuristic that improves your odds, coming up with good novel ideas is really hard and happens only rarely.)
I’ve interacted with quite a few mathematicians who readily mix raw LaTex into their emails! I have to squint but it seems to be a somewhat normal practice.