Abstract: We know that formalizing mathematics is useful. The present practise usually follows closely the style of the mathematical assistant. It would be better to follow the style of mathematics. In principle this mathematical style may change, but at present the situation is lopsided.