Lately, I’ve been spending time learning about interactive proofs using LEAN. I wanted to write a small post about it, but I felt that using only text would be a bad idea. In LEAN, proofs are built with tactics, and it is much better to see how each tactic works instead of only reading about it.

To solve this, I decided to learn Manim and use animations for explanations.

You can see a template of the future video.