learnlean

I've been studying number theory and abstract algebra as a hobby, but I got frustrated with not being able to verify my proofs, so I started learning the Lean proof assistant. There are many ways to learn Lean:

https://leanprover-community.github.io/learn.html 

Skimming the resources, the Mathematics in Lean in book clicked the best for me so I went with that: https://leanprover-community.github.io/mathematics_in_lean/index.html

Specifically, I got convinced by the Infinitely Many Primes section which is about halfway through the book. It's a simple theorem, but the rigorous proof is not trivial: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#infinitely-many-primes

OSS + Rust. I have one goal in life: the ability to stop thinking at will

how do you test your understanding of number theory and abstract algebra? is using lean the only way?

Not at all. Normally the exercises in textbooks are a good way to check understanding, but they not always have solutions + sometimes the textbooks themselves are sloppy, so I felt like it’s time to get rigorous 🤓