51²è¹Ý

Zoom Link: https://zoom.us/j/99099931387?pwd=InkqN5bH3HyHwi9eVip7IaEcZ7QP9c.1

Abstract:  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.

In 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.

In 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.

About 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.

We look forward to your active participation.