Formalizálásra szerintem úgy érdemes gondolni, mint egy módszer arra, hogy nagyon objektíven meg tudjuk mondani azt, hogy mit bizonyítottunk  és ehhez milyen feltevéseket és következtetési szabályokat használtunk.

Egyre nagyobb adatbázisok vannak teljesen formalizált komoly tételekről pl metamath, Coq, Isabelle programokkal készítik ezeket.

Ezekután a "jó-e a bizonyításom?" kérdést a számítógépemnek is feltehetem, nem kell tapasztaltabb kollegák idejét rabolni.

Nem beszélve a bizonyító és interaktív bizonyító programokról. Van olyan tétel aminek máig nem ismert "computer-free" bizonyítása. 

"mindig használjuk a "bizonyításainkban" ezt a nyelvet."

Ez nem teljesen értem. Tudsz mondani egy konkrét szituációt, amit problémásnak érzel?