Leanlang for Programmers

This is an announcement for the following workshop.

Informal Workshop: LeanLang for Programmers

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. However, as we need to know the number of participants please register by Monday, December 15, 2025 if you are interested in attending.