By formalising mathematics, not only we understand it better but we produce scientific output whose content is precisely this understanding. I will organise this argument by relating what brought m…