ICTS

Interactive Theorem Provers (or Proof Assistants) are tools that verify and partially automate mathematical proofs. The process of encoding mathematics into these systems, known as formalisation, has gained significant interest due to its role in proof verification, generating verified code for computer algebra systems, and expanding digital mathematical libraries. It seems likely with the growth in sophistication of proof assistants, and progress of Generative AI technologies, interactive theorem provers will become a useful aide for research and teaching of mathematics.  

Lean, a leading proof assistant, has grown in popularity thanks to its extensive mathlib library, which now covers most undergraduate mathematics and beyond. Notable milestones include the Liquid Tensor Experiment, which formalised a key result by Fields medalist Peter Scholze, and the rapid formalisation of the Polynomial Freiman-Ruzsa Conjecture led by Terry Tao.

The goal of the workshop is to introduce mathematicians to formalisation of mathematics using Lean. The proposed meeting will feature several talks by Lean experts, to introduce the key essentials of formalisation of mathematics using Lean, which involves reformulation of mathematical definitions and proofs to render them machine checkable.. Further, the practical sessions with concrete exercises in formalisation of mathematics, will enable participants to gain hands-on experience with formalisation in Lean.

Accommodation will be provided for outstation participants at our on campus guest house.

Eligibility criteria: The workshop is open to research students in mathematics, postdoctoral researchers, faculty members, as well as  advanced undergraduate and master’s students.

ICTS is committed to building an environment that is inclusive, non discriminatory and welcoming of diverse individuals. We especially encourage the participation of women and other under-represented groups.