I've decided to pick up Lean, a theorem prover from Microsoft research after watching Kevin Buzzard's evangelism. This was a fortuitous time for me -- I had been planning to brush up on my real analysis and measure theory (which I have honestly mostly forgotten) and I had always wanted to learn how to use a theorem prover (although I was originally planning on picking up either Coq or Isabelle). Thanks to Buzzard, it looks like formalizing real analysis using Lean is the way to go.
This is going to be my repository of various mathematicla proofs that I do along the way. Originally, I plan to mostly follow Terry Tao's Analysis textbook, but it may grow to include other branches of math.