Showcasing my first project in Lean

Stream: new members

[Weiyi Wang]

Hi all, I started learning Lean+Mathlib about two weeks ago, and I practiced by formalizing the proof of some little theorem I had a while ago (just high-school level math, for now at least). Here it is: https://github.com/wwylele/biased-bisect-lean

Things I have learned

• formalization is powerful. Before this, I have never been sure if I have got everything right in my proof and was concerned I missed something. Now with the proof written in Lean, no matter how messy it looks (lol), I know for sure it is correct.
• before proving something, sometimes the math object I described might not be well-defined in the first place, and proving the well-definedness is also important

[Martin Dvořák]

Just a small tip; the tactics unfold and rw can take multiple arguments.

[Weiyi Wang]

thanks! I am working on cleaning this up to make it look better. I am sure there are still a lot of neat features that I am not aware of