BAO Huanchen
Department of Mathematics

Huanchen documents an ongoing education project focused on using the Lean 4 proof assistant to create interactive learning games for undergraduate mathematics courses, with the goal of making formal proof technology accessible and engaging for students, particularly in challenging topics like calculus and logic.

Bao, H. C. (2025, October 27). Building interactive learning games in Lean 4: An educational project report. CTLT Teaching Connections. https://blog.nus.edu.sg/teachingconnections/2025/10/27/2025-baohc/

Over the past year, our team has been working on an education project¹ that explores how formal proof technology can support undergraduate teaching in mathematics. In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence, according to the rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. Below are sample codes showing that multiples of even integers are still even (from Mathematics in Lean by Jeremy Avigad and Patrick Massot).

More specifically for our project, we are building interactive Lean 4 games for topics in MA2002 “Calculus” and CS1231 “Discrete Structures”. The project is still in development, which has been further incorporated with student projects (the Undergraduate Research Opportunities Programme in Science [UROPS], Capstones, etc.). At the heart of the project is the idea that formal proofs—usually associated with advanced mathematics—can be turned into learning games that guide students step by step. Instead of simply listening to lectures or working through problem sets, students can interact directly with logical statements and definitions in a playful, structured environment. The Lean 4 proof assistant, with its precise language and logical rigour, provides the framework for this approach.

Why Lean 4?

Lean 4 is a modern proof assistant developed for both mathematics and computer science. The language has attracted a lot of attention from The Mathematical Society in recent years, like the formalisation of Fermat’s last theorem. Its primary purpose is to verify proofs with absolute precision, leaving no room for ambiguity. For example, while MATLAB can compute the derivative of a particular function, Lean 4 can check the correctness of a given proof of continuity.

The challenge is that Lean 4 is not an easy language to learn. For students with little or no programming experience, the syntax can be intimidating. Our project aims to lower this barrier by designing games that downplay the programming aspect and instead emphasise the mathematics. Students should not feel like they are learning a new programming language; rather, they should feel like they are exploring mathematics in a more interactive way.

The Pedagogical Goal

One of our guiding pedagogical goals is to help students better understand the epsilon-delta definition of limits in calculus. This definition is famously difficult for beginning undergraduates. Many students memorise the statement without ever truly internalising the logical structure:

For every ε > 0, there exists a δ > 0 such that if |x – a|<δ,then |f(x)- L|<ε.

Students often struggle with the “for every…, there exists…” quantifiers, as well as the nested logical reasoning required to manipulate them. We believe that an interactive Lean 4 game could make this definition less abstract and more approachable.

Our vision is a guided epsilon-delta game where students play along with the definition. For example, the game could present them with a function and a proposed limit, and then challenge them to write a rigourous proof with step-by-step guidance on the syntax.

Progress So Far

The epsilon-delta game remains in development, but we have already made significant progress in building smaller games. Currently, we have working demos in two areas:

1. Derivatives. This is closely related with the course MA2002 “Calculus”. We have designed Lean-based exercises that guide students through the definition and computation of derivatives. These exercises resemble guided examples, where students fill in missing steps in a logical chain rather than compute everything from scratch. Most examples are developed during Capstone projects for the past two semesters.
2. Basic Logic. This is closely related with the course CS1231 “Discrete Structures”. We have also created exercises that teach students the foundations of logical reasoning. These logic games ask students to prove simple statements, gradually introducing the structure of formal proofs. For many students, this doubles as training in mathematical writing and logical thinking. This part is relatively well-developed due to its simple nature in comparison with advanced concepts in Calculus.

The biggest challenge we face is balancing accessibility with rigour. On the one hand, Lean’s strength lies in its precision; on the other hand, it can quickly frustrate beginners. To overcome this, we are designing interfaces and guided prompts that hide some of the programming details while keeping the mathematics front and center.

Conclusion

This project is still in its early stages, but the potential is clear. Lean 4 provides a unique opportunity to bring formal proof technology into the undergraduate classroom, not as a hurdle, but as a playful, interactive learning tool. At the same time, developing the project itself also provides plenty of opportunities for undergraduate projects in programming.

A Demo

To give a taste of what we have built so far, we are including a short demo on an exercise from CS1231 “Discrete Structures” in this blogpost. The game can be accessed at http://10.246.80.74:3000/#/. Due to security reasons, the game server can only be accessed within the NUS network.

Endnote

1. This project was made possible due to the generous support of a Teaching Enhancement Grant (TEG) from the Centre for Teaching, Learning, and Technology (CTLT).

BAO Huanchen is an Associate Professor in the Department of Mathematics. His research focuses on the representation theory of Lie algebras, Lie superalgebras, quantum groups, and their connections to geometry and categorification. Huanchen can be reached at matbh@nus.edu.sg.