I like the idea (in fact, I used to be pretty serious about solving problems on project Euler and other such sites) but I think it is misnamed. Erdos was all a

I like the idea (in fact, I used to be pretty serious about solving problems on project Euler and other such sites) but I think it is misnamed. Erdos was all about proofs not computations. If you made the questions require proofs of general theorems, not "mere computations" then you would really have something different and cool, and appropriately named. Unfortunately, Coq is about as good as it gets when it comes to writing proofs a computer can check, and that would be no fun for anyone. I can't speak for Erdos of course, but I suspect that he would not want his name attached to such a product. He really was all about proofs.