I started learning math this year. I used Daniel Velleman's How to prove it to learn the basics of how to read and write proofs.
While doing so, I stumbled upon Velleman's companion book that uses the Lean language. I decided against starting learning it right now because I don't think I have the mental bandwidth to do so. A few months passed by and at some point I started reading my French Introduction to proof course and I saw that it mentionned a tool named edukera.
Since I don't go to class, I couldn't know for sure that we didn't need to know to use this tool so I did some exploration. I didn't like the UX of the tool but I saw that it's based on something called the Coq proof assistant...
Coq Rocq proof assistant
Rocq - which was renamed Coq for some reason - is a proof assitant [TO BE CONTINUED]