Proof Assistant based exercises and puzzles make for a good recreational activity, as well as help sharpen skills of users of said systems. There are many such equivalent resources for algorithmic puzzles (sometimes called interview problems).
Here are some resources I personally like:
You already mention two very complete sites of exercises and I don’t have much reason to think there are more of that kind. In particular, Proving For Fun hosts the proving competition Proof Ground for the conference series Interactive Theorem Proving.
However, it is still possible to find a lot of exercises out there for a number of theorem provers. They are scattered throughout books, course websites, online forums, and GitHub.
Since you are interested in mathematically deep content (as I gather from your comment), I would suggest the exercises associated with the workshop Lean For The Curious Mathematician 2020 (and soon LFTCM 2022 this summer). They are probably specific to the Lean mathlib library.
If you are interested in homotopy type theory or cubical type theory, there are tutorials with exercises:
Also, for someone like yourself who has a background in mathematics (even if is just taking a lot of math courses in college) and knows the basics of a proof assistant, I would just advise you to start to formalize real mathematics. For example, take a theorem from an undergraduate math text for which you like the proof and start to formalize it, building all the needed definitions and lemmas as you go. The nice thing about this approach is that even if your goal ends up being too ambitious, you still learn a lot along the way as you formalize the background needed for your goal. For example in 2006 I worked in formalizing group theory in HOL Light. I only got up to the first Sylow theorem and even then I never completed a key lemma involving matrices, but it was a good learning experience.
Also, it doesn't even have to be pure mathematics. I've seen people formalize theorems in Chemistry for example. Also, if verifying the correctness of algorithms is of interest to you, you could implement the algorithms from Oskaski's Purely Functional Data Structures and prove they are correct implementations.
Or better yet, just start to contribute to a formal math library like mathlib or AFP. Find a theorem prover and theorem proving community you like and ask where you can chip in on your spare time!
