Bangalore FP May 2026 meetup

Lean is a functional language used not just for writing programs but proving that they are correct.So what does it mean to “prove” something is correct exactly. Verification is the fourth step of a coming up with a solution. It means that can you prove that the solution you have come up works “reasonably” well.

In a recent hackathon at IISC bangalore, our team decided to build a small project in Lean. Our main goal was to learn about lean and apply it’s features. So we decided to go with Chess Problems. Chess problems are many - Mate in Two problems, N Queens, Knights and Knaves. We tried a few, and finally build a Chess Model in Lean, and wrote some interesting proofs for our program. Code is here: https://github.com/aastha-guptaa/Lean-Hackathon

The talk will focus on the process of building a model for Chess in Lean. In particular, it will focus on the unique features that lean offers. How functional programming helps in modelling problems like Chess. Additionally, some of our proofs actually failed. We will explore why they failed, and what that says about our particular solutions. We also built an LLM client. It suggests moves for mate in two problems, which the program then validates. Will expand on this in the talk.

Presenting Members: Malhar Patel, Rajlakshmi Chavan and Saachi Kaup. Honourary presence of Aastha Gupta.