Simon Wimmer (Jul 01 2020 at 07:40): Simon Wimmer (Jul 01 2020 at 07:40):We are happy about any feedback on Proof Ground 2020. You can also send us your feedback in private messages or via e-mail if there is anything you do not want to discuss publicly.
Some inspirations:
Manuel Eberl (Jul 01 2020 at 08:20):I would definitely like more maths problems! Scouring old International Mathematics Olympiad questions might be a good source for suitable problems, although I think you should then really give the sample solution in the problem description as well (or at least a sufficient number of hints).
I found the problem difficulty just right. The prime number one confused me because it took me quite some time to figure out how to do it "on paper". Once I did, it was trivial. With the others, the informal approach was pretty obvious and it was just a matter of getting the (routine) formalisation done (although of course there are clever ways of doing it and less clever ones, and mine were not as clever as they could have been).
Online competitions usually have the big problem that they always put people at the other end of the planet at a disadvantage, unless you let them take place over something like 16 hours or even several days, and I don't think that makes sense here. One theoretical possibility would be that there is a 1-day period or so in which a participant can "unlock" the problems and then has, say, 2 hours to solve them. As long as nobody discusses the problems with anyone else until the competition is over for everyone, that works, but one probably loses some of the online character of the competition.
Generally though, I like all three types of competition and some combination of that would be nice.
In principle, I'd be willing to help organising the competition, but of course I also want to participate, so that might clash.
As for bias, I cannot really say. Isabelle is in a good position for such competitions because of a big library, good automation, and sledgehammer. But I don't think that should count as a bias. As for the "maths" vs "CS" thing, I also don't see a bias: if anything, Isabelle probably has more material in most mathematical areas than the other system, so I don't see anything supporting the argument that focusing so much on lists, relations, etc. should favour Isabelle. But then again, I myself might be biased, of course. :big_smile:
It is, of course, possible that there would have been other problems that would have been easier to do in Lean or Coq than in Isabelle; I really cannot say. Something that calls for dependent types perhaps? Maybe it's a lack of imagination on my part, but I cannot really imagine what such a problem would look like. Someone from these other two communities is probably in a better position to judge this than I am.
Simon Wimmer (Jul 01 2020 at 08:33):Manuel Eberl said:
I would definitely like more maths problems! Scouring old International Mathematics Olympiad questions might be a good source for suitable problems, although I think you should then really give the sample solution in the problem description as well (or at least a sufficient number of hints).
I found the problem difficulty just right. The prime number one confused me because it took me quite some time to figure out how to do it "on paper". Once I did, it was trivial. With the others, the informal approach was pretty obvious and it was just a matter of getting the (routine) formalisation done (although of course there are clever ways of doing it and less clever ones, and mine were not as clever as they could have been).
Online competitions usually have the big problem that they always put people at the other end of the planet at a disadvantage, unless you let them take place over something like 16 hours or even several days, and I don't think that makes sense here. One theoretical possibility would be that there is a 1-day period or so in which a participant can "unlock" the problems and then has, say, 2 hours to solve them. As long as nobody discusses the problems with anyone else until the competition is over for everyone, that works, but one probably loses some of the online character of the competition.
Generally though, I like all three types of competition and some combination of that would be nice.
In principle, I'd be willing to help organising the competition, but of course I also want to participate, so that might clash.
As for bias, I cannot really say. Isabelle is in a good position for such competitions because of a big library, good automation, and sledgehammer. But I don't think that should count as a bias. As for the "maths" vs "CS" thing, I also don't see a bias: if anything, Isabelle probably has more material in most mathematical areas than the other system, so I don't see anything supporting the argument that focusing so much on lists, relations, etc. should favour Isabelle. But then again, I myself might be biased, of course. :big_smile:
It is, of course, possible that there would have been other problems that would have been easier to do in Lean or Coq than in Isabelle; I really cannot say. Something that calls for dependent types perhaps? Maybe it's a lack of imagination on my part, but I cannot really imagine what such a problem would look like. Someone from these other two communities is probably in a better position to judge this than I am.
I think programming competitions (e.g. Google Code Jam) usually take the approach of opening a 36 hour window to submit solutions. But yeah, without the "unlocking" that you suggest, we would just need to make much harder problems. Which would obviously be a possibility though.
maximilian p.l. haslbeck (Jul 01 2020 at 09:20):if you allow a longer time window, the time-offsets for ties in points does not make sense any more. Other than that I think it's a nice possibility.
Peter Zeller (Jul 01 2020 at 13:23):Were the problems too easy/too hard/just right?
I liked the first session better, because you could still complete one problem if you were 3 times slower than Manuel ;) In the second session I failed completely, because I spent half of the time on both problems and finished none. Might have been different if I had focused on one... I also missed somehow that task 2 was the much easier task in problem 1, because I started with task 1 and then ran out of time.
So I would have preferred if the afternoon session was the same time if the morning session, which would have made it a bit easier to at least finish one problem.
Do you prefer offline/online/or rolling competitions (e.g. like Project Euler)?
I liked the online competition. It might be an option to have a rolling competition with the same problems and a community voting, where the goal is to find the shortest or most beautiful proof. That would have a different focus and could also be used to show differences between the different tools.
Simon Wimmer (Jul 01 2020 at 14:48):Haha, yeah, Manuel is faast :D Actually, the intention of the second session was to make it kind of competitive for him.
But it's true that it may be more motivating if there is a low hanging fruit in every session.
Actually, that's an interesting suggestion on bringing in different criteria. Maybe we could do this for all existing solutions: there could be a closed forum for all those who solved a problem where you could upvote solutions. However, this would also reach way too far given the number of users we have currently...
Manuel Eberl (Jul 01 2020 at 14:54):Yeah I think we seriously need to try to bring more people to PG. Given the size of the Isa/Coq/Lean communities, the participation was quite meagre.
Manuel Eberl (Jul 01 2020 at 14:54):Maybe participation in PG should be mandatory for all ITP attendants. :P
Manuel Eberl (Jul 01 2020 at 14:55):Every attendant must solve at least one problem, every attendant with a talk at least 2. ^^
Lukas Stevens (Jul 01 2020 at 15:01):Simon Wimmer said:
Haha, yeah, Manuel is faast :D Actually, the intention of the second session was to make it kind of competitive for him.
But it's true that it may be more motivating if there is a low hanging fruit in every session.Actually, that's an interesting suggestion on bringing in different criteria. Maybe we could do this for all existing solutions: there could be a closed forum for all those who solved a problem where you could upvote solutions. However, this would also reach way too far given the number of users we have currently...
That is also what ACM competitions do. There are a lot of tasks and some of them are quite easy. Of course, only the fastest will solve all tasks.
Lukas Stevens (Jul 01 2020 at 15:02):Are team competitions using one computer per team also on the table?
Simon Wimmer (Jul 01 2020 at 15:04):Yeah, in general, I would be open to that, and we allowed it last time. But given that we had the online format anyway this time, we wanted to separate Manuel and Peter to make it more interesting ;) I don't know what others think about it this.
Manuel Eberl (Jul 01 2020 at 15:06):You could have just asked us not to team up. :D
maximilian p.l. haslbeck (Jul 02 2020 at 08:08):we did
Manuel Eberl (Jul 02 2020 at 12:50):Okay I promise never to team up with Peter again. ^^
maximilian p.l. haslbeck (Jul 02 2020 at 16:29):Manuel Eberl said:
Okay I promise never to team up with Peter again. ^^
never say never. and I suppose you restrict that to proof ground, and not apply it to climbing :D
Simon Hudon (Jul 02 2020 at 16:30):To make it more challenging for everyone, you might want to pick a different prover than Isabelle ... and still team up with Peter
maximilian p.l. haslbeck (Jul 02 2020 at 16:31):that's actually nice. A competition where you are not allowed to use your favourite prover ^^
maximilian p.l. haslbeck (Jul 02 2020 at 16:31):or teaming up two participants of different provers
Manuel Eberl (Jul 02 2020 at 20:07):Yeah I'd be really lost then. I've wanted to branch out into another system for years, but never actually got around to doing it.
Last updated: Dec 22 2024 at 12:33 UTC