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

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 🤓

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