TT is politely and gently trying to deal with the ego of many mathematicians, namely to teach them humility, which they will need to design their specialized maths AI models(agents?). Well, dunno if it will work out anything interesting, but he is giving a try.

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.