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 .
