iTranslated by AI
Enjoy Chomp in Lean this Christmas
This is the article for Day 16 of the Theorem Prover Advent Calendar 2025.
However, this article will not deal with the intricacies of formal proof.
General-Purpose Programming Language Lean
The Lean language is a general-purpose functional programming language (that somehow also allows you to describe proofs of mathematical theorems). As such, you can write regular programs with it. It incorporates monads and their do notation, allowing you to write code in a style similar to imperative programming languages.
In this article, we will implement the Poison Chocolate Game (Chomp) as a command-line game using Lean and enjoy playing it.
Poison Chocolate Game: Chomp
The Poison Chocolate Game is a wonderful game for two players, where you take turns trying to force your opponent to eat the piece of chocolate that contains poison.
For detailed rules, please watch the video "Winning Strategy for the Poison Chocolate Game [Yukkuri Commentary]" on the YouTube channel "Ebima Lab."
Chomp Program (Generated by LLM)
Nowadays, programs of this scale can be created by generative AIs like ChatGPT and Gemini.
The following code was created by Gemini. I corrected two grammatical errors (specifically, how elements are retrieved from a list).
/-- Game settings: width and height -/
def width : Nat := 5
def height : Nat := 4
/-- Board state
A list of the heights (number of pieces) of chocolate remaining in each column -/
abbrev Board := List Nat
/-- Create initial board -/
def initBoard : Board := List.replicate width height
/-- Display the board -/
def printBoard (b : Board) : IO Unit := do
IO.println " 0 1 2 3 4 (列)"
IO.println " -----------"
for r in [0:height] do
let mut line := s!"{r}| "
for c in [0:width] do
-- If the height of that column is greater than the current row r, there is chocolate
if let some h := b[c]? then
if r < h then
line := line ++ "O "
else
line := line ++ ". "
else
line := line ++ " "
IO.println line
IO.println ""
/-- Parse input -/
def parseInput (s : String) : Option (Nat × Nat) := do
let parts := s.trim.splitOn " "
match parts with
| [rStr, cStr] =>
let r ← rStr.toNat?
let c ← cStr.toNat?
some (r, c)
| _ => none
/-- Move logic
Removes all chocolate to the lower right of the specified (r, c).
Traverses the list from the beginning and does nothing until the specified column c is reached.
From column c onwards, limits the height by r (min). -/
def makeMove (b : Board) (r c : Nat) : Board :=
match b with
| [] => []
| h :: t =>
if c > 0 then
-- To the left of the specified column, so height h remains as is. Move to the next column (decrement c)
h :: makeMove t r (c - 1)
else
-- From the specified column onwards, height becomes min h r. Maintain c at 0 to apply to everything on the right
min h r :: makeMove t r 0
/-- Main game loop -/
partial def gameLoop (b : Board) (player : Nat) : IO Unit := do
printBoard b
let playerNum := player + 1
IO.println s!"プレイヤー {playerNum} の番です (行 列 を入力, 例: 1 2): "
let stdin ← IO.getStdin
let input ← stdin.getLine
match parseInput input with
| some (r, c) =>
let colHeight := b[c]!
if c >= width || r >= height then
IO.println "エラー: 範囲外です。もう一度入力してください。"
gameLoop b player
else if r >= colHeight then
IO.println "エラー: そこにはもうチョコがありません。"
gameLoop b player
else if r == 0 && c == 0 then
IO.println s!"\n!!! 毒(0,0)を食べました！ プレイヤー {playerNum} の負けです !!!"
else
let newBoard := makeMove b r c
gameLoop newBoard (1 - player)
| none =>
IO.println "エラー: '行 列' の形式で数字を入力してください。"
gameLoop b player
/-- Entry point -/
def main : IO Unit := do
IO.println "=== CHOMP ゲームへようこそ ==="
IO.println "左上の (0, 0) を食べると負けです。"
IO.println "右下の領域を消していきます。\n"
gameLoop initBoard 0
How to Play
-
If you haven't installed Lean yet, please do so.
https://lean-lang.org/install/ -
Save the Lean source code above as
ChompGame.lean. -
Run it using the
leancommand.
lean --run ChompGame.lean
Execution Example
$ lean --run ChompGame.lean
=== Welcome to the CHOMP Game ===
You lose if you eat the (0, 0) at the top-left.
We will clear out areas toward the bottom-right.
0 1 2 3 4 (col)
-----------
0| O O O O O
1| O O O O O
2| O O O O O
3| O O O O O
It is Player 1's turn (Enter row col, e.g., 1 2):
1 2
0 1 2 3 4 (col)
-----------
0| O O O O O
1| O O . . .
2| O O . . .
3| O O . . .
It is Player 2's turn (Enter row col, e.g., 1 2):
2 0
0 1 2 3 4 (col)
-----------
0| O O O O O
1| O O . . .
2| . . . . .
3| . . . . .
It is Player 1's turn (Enter row col, e.g., 1 2):
0 1
0 1 2 3 4 (col)
-----------
0| O . . . .
1| O . . . .
2| . . . . .
3| . . . . .
It is Player 2's turn (Enter row col, e.g., 1 2):
1 0
0 1 2 3 4 (col)
-----------
0| O . . . .
1| . . . . .
2| . . . . .
3| . . . . .
It is Player 1's turn (Enter row col, e.g., 1 2):
0 0
!!! You ate the poison (0,0)! Player 1 loses !!!
Is Chomp a First-Player Win?
By the way, according to the "Ebima Lab" video, this Poison Chocolate Game (Chomp) is a first-player win game. Since Lean is a theorem prover, I would like to prove this fact using it.
I plan to post an article about the proof at a later date. Please stay tuned.
(Update) I have proved it.
Discussion