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.
Apply by using the form. Student applicants seeking financial support should apply early — spots are limited.
Registration is closed
Enrollment is closed
DEADLINE FOR STUDENTS SUPPORT IS CLOSED
Students support notifications
Registration is closed
Notification shared to the selected participants
Participation Confirmed
Indian Institute of Science
(IISc, Bengaluru, India)
Indian Institute of Science
(IISc, Bengaluru, India)
Indian Institute of Technology Madras
(IIT–Madras)
National University of Singapore
(NUS)
Over five inspiring days, the Summer School brought together programmers, mathematicians, and curious learners to explore the world of Lean—from the fundamentals to advanced techniques in formal verification. A standout session featured Prof. Ilya Sergey introducing participants to proving real-world imperative programs in Lean using the Velvet framework developed in his lab.
A heartfelt thank you to our keynote speakers — Siddhartha Gadgil, KC Sivaramakrishnan, Komondoor V Raghavan, Ilya Sergey, Deepak D'souza —for sharing their knowledge, experience, and insights throughout the Summer School.
From hands-on labs and interactive tutorials to inspiring talks and open Q&A sessions, participants didn't just learn Lean—they experienced it by building, experimenting, and collaborating alongside some of the field's leading experts.
