Contemporary Formal Mathematics (Part I)

Arithmetic is at the dawn of any scientific discipline. In our life we all have experienced (doing calculation) the validity of the following kind of equality 1947+1789 = 1789+1947 = 3736. It is less clear that every scientist has ever proved this property of commutativity in the general case. Following the custom of the student seminar, we will altogether construct a very precise proof of this property. It will be conducted in a context of contemporary formal mathematics, in such a way that a stupid (but powerful) computer can check the proof. The consequence of this work in our everyday life is enormous, instead of saying "I believe that the addition is commutative" one will now be proud to say "I know that the addition is commutative".