Have you thought an interactive site where people could learn coq writing proofs? Something very similar to https://projecteuler.net/. You could get thousands of failed proofs very fast.
That's a neat idea. It would mostly help for gathering data from beginners, which would be very skewed, but I'm sure it could still be useful, especially for developing tools to help beginners.
Yeah skewing would be definitely problematic, it might be better if it would be similar to Kaggle where people would compete with each other.
This is a great idea. As I interested novice I'd certainly be a early adopter.