I have 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

6

2026-06-20

I started working on the interactive book Mathematics in Lean and finished S01_Calculating. I originally thought it was a little challenging, but now I am getting used to it and starting to enjoy it. The Lean games helped get me familiar with the syntax and build my confidence. The book provides a development environment in VS Code for Lean so I can expore more freely and prepare for more advanced topics. I am excited to continue learning and exploring the world of Lean!

5

2026-06-19

After around 13 hours of reading, I have completed The Proof in the Code. The book provided a great overview of the history and development of Lean, as well as insights into the Lean community. I learned about the challenges and successes of the early adopters of Lean and how they contributed to its growth. I am inspired by their dedication and passion for formalizing mathematics. I will continue to explore Lean and apply what I have learned from the book.

4

2026-06-15

I bought the newly published book The Proof in the Code and started reading it. The book is very well written and provides a great story of the birth and evolution of Lean. It also provides a lot of insights into the Lean community and its culture. I am excited to read more and learn from the experiences of the important figures in the community.

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.

📓 I am also keeping a note on Lean for Mathematics with LaTeX formulas and Lean code.