I wonder if the current maths models, if any, are able to use formal solvers in their 'reasoning'. I wonder if a natural language interface is really that efficient, maybe a pure formal language hinted with intuitive "tokens". I remember the time I was learning real maths: "elegant", "brutal", "strong", etc were somewhat meaningfull.

    ....-----

    ---/Shark\---Terry Tao

No matter how good your case is - if you use AI slop to spam text, I will not read it. At the least they admitted to this sneaky slopness, which saves me time. I'd wish everyone would do so.