Lean (or Lean Prover) is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code. There has been a lot of interest in Lean recently, especially with the hope that it can enable AI to be used reliably in mathematics, software and beyond.

We will have a one-day informal workshop on Lean on Friday, 19 December at the the Indian Institute of Science, Bangalore, with a focus on programming, aimed at software professionals among others. The workshop will consist of example based introductions to various aspects of Lean and exercises to work on with help. The two principal speakers are Siddhartha Gadgil and Anand Rao Tadipatri.

The workshop is free and is funded under a grant from Renaissance Philanthropy.

Details

Schedule

Installing Lean and Workshop repository

The workshop will include live coding as well as lab sessions where participants work with help on exercises. It is recommended that you bring a laptop with Lean installed and the workshop repository cloned. The following are instructions to do this.

I. Installing VS Code and Lean 4: Follow the official instructions, install visual studio code and the Lean 4 plugin and test the installation is working. Warning: You must choose the “Lean 4” plugin (called lean4), not the “Lean 3” one (called lean).

II. Downloading the workshop repository: As you have seen in the previous step, the menu for the Lean 4 plugin is at the ∀ symbol.

  1. At the Lean4 (i..e, ∀) menu, choose “Open Project”, then “Download project” (as in the screenshot below).Open Lean Project

  2. Choose the repository https://github.com/siddhartha-gadgil/LeanLangur (see the screenshot below).Open Workshop Repository

  3. Open the file LeanLangur/Basic.lean to check that the installation has worked.


Contact: +91 (80) 2293 2711, +91 (80) 2293 2265 ;     E-mail: chair.math[at]iisc[dot]ac[dot]in
Last updated: 16 Jan 2026