If my purpose of using Coq is purely mathematical, what are the most suitable resources can I learn Coq from?

I am currently studying math but am very interested in using Coq. If my purpose of using Coq is purely mathematical, what are the most suitable resources can I learn Coq from? For example, my purpose can be just to prove the fundamental theorem of calculus in Coq by myself and let Coq check my proof.

I would suggest one of the books from Coq’s documentation. The last one by Mahboubi and Tassi is especially geared towards mathematicians.

1 Like