Two days ago, I decided to learn Lean. My goal is to contribute to Mathlib and the mathematic commutinity, and formalize my recently published paper On the stability and instability of Kelvin–Stuart cat’s-eye flows (Inventiones Mathematicae).

 

This page is to record my journey and motivate myself.

Id Date notes

3

2026-06-01

The interactive book was not suitable for me. I need more basic resources to get started. The Natural Number Game helped me get started with the basics of Lean and understand how to use it for simple proofs. I found it very interesting and engaging. I have completed Tutorial World and Addition World. I will continue to explore the other worlds and practice more with Lean. I am excited to see how far I can go with this!

2

2026-05-30
  • Found helpful resources including the interactive book Mathematics in Lean and online video series Introduction to Formalization and Lean 4 on YouTube.
  • Joined the Lean community Zulip and set up VS Code to run the interactive book. I need to get used to the syntax and commands. But it’s exciting to see how Lean can formalize mathematical concepts and proofs.
  • Excited to dive deeper into the world of Lean and play with math in a different way!

1

2026-05-29

Today marks the beginning of my Lean journey.