Checkmate by Proof: A Chess System in Lean

Lean is a functional programming language that lets you write programs and prove properties about them in the same language. But what does it actually mean to prove that a program is correct?

At the Lean Hackathon at IISc Bangalore, our team set out to answer that question by building a chess system from scratch in Lean. We modeled pieces, positions, and the rules of movement, and built a system that could validate moves and reason about checkmate.

We'll discuss what it means to verify software beyond writing tests and how we proved properties about our chess model instead of simply assuming they were true.

This talk is about using Lean as a programming language: how its type system and proof capabilities influence software design, what it feels like to build a real system in it, and why these ideas matter to the broader programming languages and systems community.

Repository Link: https://github.com/aastha-guptaa/Lean-Hackathon
Presenting Members: Malhar Patel, Aastha Gupta, Rajlakshmi Chavan, and Saachi Kaup.

• Understanding the basics of formal verification through a practical Lean project.

• Modeling and reasoning about a real-world system using functional programming and expressive types.

• Exploring how theorem proving can complement traditional software development and testing.