Recently our hackathon team presented work for the lean hackathon at an FP meetup. It was super fun. I was lucky enough to meet a group of extremely talented people. From different backgrounds - maths and economics. But what did we work on exactly?

Since Lean was a new language for us, we decided to tackle a simpler problem. Chess! Incidentally, for the WE program a few years ago, one of my first bigger projects had been a chess engine. I don’t play chess. I know the rules of it, barely. But anyways. The Chess project we chose was because mainly we wanted to see what we could prove about our system. Reliably. 

So we made a chess system which does the following:

Using the FEN notation (a common chess notation). It uses this to provide the initial board state effectively to the system. We then ask an LLM hey look at this board, and tell me can you suggest in 2 moves can we do a checkmate. And it has to be a forced move for the king in the next move, resulting in checkmate. 

Our chess model is defined with structures for ColourPiece, Square, Board, Pos etc. Then with lean, our model shows if the move provided by the LLM is a valid move or not, and if it results in checkmate or not. For this we have two divisions: Pseudolegal moves (all possible allowed moves) and legal moves(moves which result in checkmate). We make sure the LLM gives us a reliably formatted output with structured outputs: https://developers.openai.com/api/docs/guides/structured-outputs.

But first, we have to have properties proven about our system. I will explain a simple proof. We have a function called isInCheck :

def isInCheck (state : GameState) (colour : Colour) : Bool :=

match findKing state.board colour with

| none => true -- malformed board: treat as unsafe

| some kPos => isSquareAttacked state.board colour.opponent kPos

We also have a isSquareAttacked function which checks if the target attacked by any piece of colour attacker on the board. A few interesting parts on how that is defined:

let rec loop (i fuel : Nat) : Bool :=

   match fuel with

…

 loop (i + 1) fuel'

  loop 0 64

rec keyword defines the function loop, which loops through all the squares. And it MUST be reliably terminating. Interestingly, here is another example from the lean docs. The Nat keyword is for Natural numbers. Integers are not enough. Some good examples I found were::

-- This works: clearly structural

def sum : List Nat → Nat

  | [] => 0

  | x :: xs => x + sum xs

  
-- This needs a hint: n / 2 is smaller, but Lean can't see it

def collatz (n : Nat) : Nat :=

  if n ≤ 1 then n

  else if n % 2 == 0 then collatz (n / 2)

  else collatz (3 * n + 1)

termination_by n

decreasing_by sorry  -- We're cheating here—Collatz termination is unproven!

I tried this out. It doesn’t COMPILE. Recursion, the ability of a function to call itself, is basically the fundamental building block of programming. A similar program in Haskell or python would have worked just fine. But we can get around this with the partial keyword:

partial def collatz (n : Nat) : Nat :=

 if n ≤ 1 then n

 else if n % 2 == 0 then collatz (n / 2)

 else collatz (3 * n + 1)

This works. Might go on forever, but works. Digression done, back to the point, our proofs. Our theorem looks like this:

theorem isInCheck_eq_attackedKingSquare

 (s : GameState) (c : Colour) (k : Pos)

 (h : findKing s.board c = some k) :

 isInCheck s c = isSquareAttacked s.board c.opponent k := by

 unfold isInCheck

 simp [h]

VSCode provides a good execution environment for lean. Writing that sentence hurt me deeply. But we must live. So if you right click on the unfold part in the proof, it breaks down the steps in the InfoView. That looks like this:

**s** : GameState

**c** : Colour

**k** : Pos

**h** : findKing s.board c = some k

**⊢** (match findKing s.board c with | none => false | some kPos => isSquareAttacked s.board c.opponent kPos) = isSquareAttacked s.board c.opponent k

The unfold part is effectively opening up the function to it's definition. So lean is then able to look inside the isInCheck function to the match findKing.. function call. Then comes simp. The easiest way I have understood simp is that it simplifies your goal. It reduces what you want to achieve to it's simplest form. Again, some refs came to the rescue:

example (n : Nat) : n + 0 + 0 + 0 = n := by

simp -- Removes all the + 0s automatically

example (a b c : Nat) : a + b + c + 0 = c + (b + a) := by

simp [Nat.add_comm, Nat.add_assoc]

-- Simplifies and uses commutativity/associativity

And so our proof is expanded by unfold and simplified. For our colour, if the board isInCheck, the opponent is attacking our king. These are two different functions, and we are proving things about Chess by connecting them.

To note, this is all done for the already defined system. We have defined a system, we are proving things about it. Our system could still have bugs that slip through ofcourse, but this is a different way of looking at it. 

Many more proofs were there, most of which, quite frankly, my math wiz teammates would explain better. Some highlights were as follow - bishop_stays_on_colour which proves that whenever a bishop moves, the colour of the square doesn’t change. And no_friendly_fire. It proves that a valid target square can never contain a friendly piece. We know such properties can be proven about our system. Pretty cool.

That is about it. I have a lot more to learn. Have barely barely barely scratched the surface. Am still not even sure I understand all of it. But I am very happy to have attempted this , and to have learnt so much more than I could have imagined.

My mentor Asokan pichai shared this article. This talks about transition invariants within chess. Perhaps we could include such proofs also.

Malhar, our amazing teammate also proceeded to make a much better system after the pressure of the hackathon ended. Have a look here. It reminded me of what I love about programming. Good functional programming always does.

Thank you to Aastha Gupta as well, for always keeping our team on track. And to Rajlakshmi Chavan for all her help. I am very proud of the work we have, small as it may be.

Anyways, a small toast. To learning from and with other people!

Refs

1. This resource is a good start
   
2. Unfold, but also tactics in general in lean
3. Functional Programming in Lean