Why formalize mathematics – more than catching errors