BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Ashoka University - ECPv6.18.4//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Ashoka University
X-ORIGINAL-URL:https://www.ashoka.edu.in
X-WR-CALDESC:Events for Ashoka University
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Asia/Kolkata
BEGIN:STANDARD
TZOFFSETFROM:+0530
TZOFFSETTO:+0530
TZNAME:IST
DTSTART:20250101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Asia/Kolkata:20260129T133000
DTEND;TZID=Asia/Kolkata:20260129T144500
DTSTAMP:20260128T023445Z
CREATED:20260128T023445Z
LAST-MODIFIED:20260128T023445Z
UID:88926-1769693400-1769697900@www.ashoka.edu.in
SUMMARY:CS and Maths Colloquium
DESCRIPTION:Zoom Link: https://zoom.us/j/99099931387?pwd=InkqN5bH3HyHwi9eVip7IaEcZ7QP9c.1 \nAbstract:  Interactive Theorem Provers (ITPs)\, or proof assistants\, can be thought of as digital proof readers that check proofs with machine-level certainty. In return for these guarantees\, proofs and programs must be written in a precise formal language\, typically based on type theory. Translating ordinary mathematical arguments and program specifications into such machine-checkable form\, a process known as formalisation\, requires making implicit reasoning explicit and carefully representing mathematical and computational objects. \nIn the the first of this session\, we survey the landscape of interactive theorem proving: its historical development\, why machine-checked proofs and verified programs matter today\, and how encoding mathematics and computation in type-theoretic frameworks differs from traditional set-theoretic approaches\, and how interactive theorem provers differ from Automated Theorem Provers\, and the relationship betweens proofs and programs.  We situate Lean within the broader ecosystem of proof assistants\, including Agda\, Isabelle\, Mizar\, and Rocq\, and discuss its design choices and trade-offs. We also briefly examine the opportunities and limitations of AI-assisted formalisation. \nIn the second half\, we give a hands-on introduction to Lean\, a modern proof assistant with a large mathematical library. Participants will see how definitions\, programs\, and proofs are developed interactively\, and how Lean supports both programming and proving within a unified framework. No prior experience is assumed; the goal is to provide orientation and a concrete entry point into the formalisation of programs and proofs. \nAbout the Speaker:  T. V. H. Prathamesh is an Assistant Professor of Computer Science at Krea University. His research lies in computational logic\, with a focus on formalisation in type theory and machine-checked proofs in mathematics and theoretical computer science. He has contributed to formal developments in knot theory\, term rewriting\, tree automata\, combinatorial group theory\, and combinatorial geometry using proof assistants. He holds an Integrated PhD in Mathematics from the Indian Institute of Science and has held postdoctoral positions at the Institute of Mathematical Sciences and the University of Innsbruck. \nWe look forward to your active participation.
URL:https://www.ashoka.edu.in/event/cs-and-maths-colloquium/
END:VEVENT
END:VCALENDAR