BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1106
DTSTAMP:20230914T125950Z
SUMMARY:Formalizing Finite Set Combinatorics in Type Theory
DESCRIPTION:Speaker: Abhishek Singh\n\nAbstract: \nMathematical proofs when
written in conventional ways often contain imprecise definitions\, unstat
ed background assumptions\, and inferential gaps in reasoning. In such cir
cumstances\, it becomes difficult for a reviewer to determine whether the
given proof is correct or not. Even if the theorem statement turns out t
o be true\, judging it to be so could take a long time. A possible solutio
n to this problem is to formalize mathematical results using Proof Assista
nts. Proof Assistants are software tools built on top of a small and trust
ed kernel that provides a formal language for writing mathematical stateme
nts and their proofs. Hence\, formally verifying a mathematical theory usi
ng a Proof Assistant can increase our confidence in the verified results.
However\, the task of formalizing mathematics using Proof Assistants prese
nts some unique challenges\; both practical as well as theoretical. Theore
tical challenges mostly arise because some trivially assumed axioms of cla
ssical mathematics may not be provable in the core logic of the Proof Assi
stant. On the other hand\, the practical difficulties of formalization mos
tly arise because the machine-checkable proofs are significantly more deta
iled than the corresponding paper proofs. In this talk\, we will address b
oth these issues while presenting formal proofs of some key results from f
inite set combinatorics. More precisely\, we present formalized libraries
of definitions and results on two important mathematical structures from c
ombinatorics: (i) finite partially ordered sets\, and (ii) finite simple g
raphs. These libraries have been formalized in the type theory of Coq Proo
f Assistant.\n\nZoom Link:\nhttps://zoom.us/j/95365190349?pwd=ZENsRG1pbmVp
V01nQ3BPRGJVZmZPdz09\nMeeting ID: 953 6519 0349\nPasscode: 993493\n
URL:https://www.tcs.tifr.res.in/web/events/1106
DTSTART;TZID=Asia/Kolkata:20201214T103000
DTEND;TZID=Asia/Kolkata:20201214T113000
END:VEVENT
END:VCALENDAR