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