Mini Course: Mathematical Programming and Reasoning in Lean

In this tutorial, participants will be introduced to the Lean proof assistant as both a programming environment and a platform for formal mathematical reasoning. Students will learn how to implement number-theoretic and combinatorial functions, such as the Fibonacci and Catalan sequences. A distinctive feature of Lean is that programs and proofs coexist in the same framework. Beyond computing values, participants will learn how to formally state mathematical claims about their definitions and develop proofs that are fully verified by the system. Through guided, interactive exercises, the tutorial will demonstrate how computation and proof can inform and reinforce one another.