Summer School: LeanLang for Programming

As the use of Artificial Intelligence tools for generating programs, proving mathematical results, and many other applications have become widespread, it has become imperative to ensure that the outputs produced by AI are correct. LeanLang, which is an open-source programming language and proof assistant, is a promising way to ensure this across fields, and is increasingly being used to verify AI-generated output. It has also been used for verification in output independent of AI, notably in authentication by Amazon Web Services and in the verification of major mathematical results, including pathbreaking mathematical work of Peter Scholze.

To introduce programmers, mathematicians, and all curious people to Lean, and sharpen the skills of Lean users, we will be organizing a summer school at the Indian Institute of Science, Bengaluru, from July 6 to July 10, 2026. This will focus on proving, programming and proving programs in Lean. A highlight of the summer school is an introduction to proving imperative programs, hence typical real-world programs, in Lean by Ilya Sergey using the framework Velvet developed in his lab. We will also have keynote talks by leading experts in formal verification.

Most of the workshop will consist of lab sessions where participants learn by working hands-on on exercises with help from experts, and Q & A sessions for freewheeling discussions and impromptu tutorials.