I am a CS undergrad highly interested in learning math relevant to my field. The math courses at my university were informal and minimal. Unsatisfied, I started working through Terence Tao's Analysis I. While I enjoyed reading the book, doing exercises was a painful experience. Since I wanted to make sure that my solutions are formal, I had to check them myself many times and in the end I still wasn't sure if they were right. I only completed a few chapters.
Having a background in competitive programming I desired a tool to validate my proofs, similar to online judges. I learned about Coq and started working through Software Foundations. I've really enjoyed the exercises so far, but recently I realized that Coq's math is different from the one in Tao's book. For example Peano's axioms can be proved in Coq.
I am wondering if these differences keep being relevant throughout the whole analysis or they only matter while working close to the axioms?
And this raises my more general question: from the educational point of view, does it make sense to use Coq to learn math on my level?