BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1040
DTSTAMP:20230914T125948Z
SUMMARY:Formalizing Finite Set Combinatorics in Type Theory
DESCRIPTION:Speaker: Abhishek Singh\n\nAbstract: \nAbstract: Mathematical p
 roofs when written in conventional ways often contain imprecise definition
 s\, unstated background assumptions\, and inferential gaps in reasoning. I
 n such circumstances\, it becomes difficult for a reviewer to determine wh
 ether the given proof is correct or not.  Even if the theorem statement t
 urns out to be true\, judging it to be so could take a long time. A possib
 le solution to this problem is to formalize mathematical results using Pro
 of Assistants. Proof Assistants are software tools built on top of a small
  and trusted kernel that provides a formal language for writing mathematic
 al statements and their proofs. Hence\, formally verifying a mathematical 
 theory using a Proof Assistant can increase our confidence in the verified
  results. However\, the task of formalizing mathematics using Proof Assist
 ants presents some unique challenges\; both practical as well as theoretic
 al. Theoretical challenges mostly arise because some trivially assumed axi
 oms of classical mathematics may not be provable in the core logic of the 
 Proof Assistant. On the other hand\, the practical difficulties of formali
 zation mostly arise because the machine-checkable proofs are significantly
  more detailed than the corresponding paper proofs. In this talk\, we will
  address both these issues while presenting formal proofs of some key resu
 lts from finite set combinatorics. More precisely\, we present formalized 
 libraries of definitions and results on two important mathematical structu
 res from combinatorics: (i) finite partially ordered sets\, and (ii) finit
 e simple graphs. These libraries have been formalized in the type theory o
 f Coq Proof Assistant.\n
URL:https://www.tcs.tifr.res.in/web/events/1040
DTSTART;TZID=Asia/Kolkata:20200115T113000
DTEND;TZID=Asia/Kolkata:20200115T130000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR