BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/80
DTSTAMP:20230914T125909Z
SUMMARY:Contemporary Formal Mathematics (Part I)
DESCRIPTION:Speaker: Benoit Razet\nTata Institute of Fundamental Research\n
School of Technology and Computer Science\nHomi Bhabha Road\n\nAbstract: \
nArithmetic is at the dawn of any scientific discipline. In our life we al
l have experienced (doing calculation) the validity of the following kind
of equality 1947+1789 = 1789+1947 = 3736. It is less clear that every scie
ntist 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 powe
rful) computer can check the proof. The consequence of this work in our ev
eryday life is enormous\, instead of saying I believe that the addition i
s commutative one will now be proud to say I know that the addition is c
ommutative .\n
URL:https://www.tcs.tifr.res.in/web/events/80
DTSTART;VALUE=DATE:20100326
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR