Tata Institute of Fundamental Research
Contemporary Formal Mathematics (Part I)
Student Seminar
Speaker:
Benoit Razet
Tata Institute of Fundamental Research
School of Technology and Computer Science
Homi Bhabha Road
Date:
Friday, 26 Mar 2010 (all day)
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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 .
| Speaker: | Benoit Razet Tata Institute of Fundamental Research School of Technology and Computer Science Homi Bhabha Road |
| Date: | Friday, 26 Mar 2010 (all day) |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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 .