I learned working with the Isabelle proof assistant in a university course. There were weekly exercises and a group project at the end. (Actually proving things by hand, no LLM.) That really helped. Before that course it was also hard for me to get into this.

Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.