Re: [isabelle] Proving Contests

```Instead of judging by proof by runtime (which does not seem like a very
useful criterion) or by beauty (which needs big human effort), an option
would be percentage of completion. By giving out several problems of
differing hardness one could make sure that basically no-one will get 100%
of the solutions. (And even for a given problem one might have different
options. E.g., prove this for integers vs. for any ring. Or prove this with
the following additional simplifying assumption vs. prove it without
assumption, etc.)

Then checking can be automated. (And to look for cheaters, it will not be
enough to manually scan the source for for "sorry". Instead, the only
reliable way as far as I know is to extract the proof term and replay it in
a separate instance of Isabelle. But the infrastructure for that is mostly
there, so it's mainly a question of filling in some "plumbing".)

Best wishes,
Dominique.

On Wed, 7 Nov 2018 at 10:14, Gidon Ernst <gidon.ernst at unimelb.edu.au> wrote:

> Hi José,
>
> indeed, judging the solutions in those competitions was always a
> tremendous effort.
> The reason why at these events humans had to be involved in the judging
> was the diversity of tools and the fact that specifications were given in
> natural language.
>
> Your idea is quite different and very intriguing! I hope it will be
> realized eventually :)
>
> Best,
>   Gidon
>
> ________________________________________
> From: cl-isabelle-users-bounces at lists.cam.ac.uk <
> cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of José Manuel
> Rodriguez Caballero <josephcmac at gmail.com>
> Sent: Wednesday, November 7, 2018 4:54:25 PM
> To: cl-isabelle-users at lists.cam.ac.uk
> Subject: Re: [isabelle] Proving Contests
>
> Hi Gidon,
>
> Interesting Proving Contests in your links, thank you ! Nevertheless, I
> took a look at the Geographical distribution of the participants (page 3 in
>
>
> I think that it is important to open a competition for millions of
> participants at the same time, including participants from less
> economically developed countries. This is the reason why I suggested a
> software in order to do the ordering of the solutions in virtue of the
> running time: human cannot handle such a huge data.
>
> In the same way that alphabetization was extended from an elite to the
> whole world, proof assistants are a second alphabetization that the world
> need in order to get update: https://www.youtube.com/watch?v=7Pq-S557XQU
>
> Kind Regards,
> José Manuel Rodriguez Caballero
>
>
> El mar., 6 nov. 2018 a las 21:26, Gidon Ernst (<gidon.ernst at unimelb.edu.au
> >)
> escribió:
>
> > Hi all,
> > two similar competitions come to mind:
> >
> > 1st and 2nd VSComp, see
> > The 1st verified software competition: Experience report, FM2011
> > The 2nd verified software competition: Experience report, COMPARE 2012
> >
> > VerifyThis (yearly at ETAPS)
> > http://www.pm.inf.ethz.ch/research/verifythis.html
> > This year, the Isabelle Team from TUM took the gold medal :)
> > Huisman, Klebanov, Monahan: On the organisation of program verification
> > competitions, COMPARE 2012
> > the yearly competition reports, and the STTT 17(6) special issue:
> >
> > Hope you find this information useful :)
> >
> > Best,
> >   Gidon
> >
> > ________________________________________
> > From: cl-isabelle-users-bounces at lists.cam.ac.uk <
> > cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of José Manuel
> > Rodriguez Caballero <josephcmac at gmail.com>
> > Sent: Wednesday, November 7, 2018 10:59:06 AM
> > To: cl-isabelle-users at lists.cam.ac.uk
> > Subject: [isabelle]  Proving Contests
> >
> > >
> > > max wrote:
> > > Just now we anounced the contest system,
> > > which we are using for managing homework submissions for
> > > the current Semantics course here at TUM, as well as providing
> > > a (short) tutorial to Isabelle and the system.
> > > Also, we host monthly contests with relatively easy but hopefully
> > > fun problems. I'm already looking for problems for the month of
> > > December. I think the goal should be that experienced Isabelle
> > > users can solve them within 30 minutes.
> >
> >
> > Nice project. My idea of an International Olympiad in Isabelle are a
> little
> > bit different. Indeed, I can summarize my vision as follows:
> >
> > 1) There will be some publicity about the International Olympiad some
> > months before its date. The publicity should be mainly addressed to
> > undergraduate and high school students. People interested in the Olympiad
> > should summit their email addresses in a website. People working with
> > Isabelle in an official research project, e.g., a Master, a PhD, a
> > professor or a professional programmer, are not allowed to apply in order
> > to guarantee more space for beginners.
> >
> > 2) The day of the Olympiad, a thy-file with a theorem followed by sorry
> > will be sent to each one of the email addresses.
> >
> > 3) People can submit their solutions until 6 hours after their received
> the
> > email  with the problem (5 hours to solve the problem and 1 hour to make
> a
> > break, I guess). Solutions sent after the deadline will be automatically
> > ignored.
> >
> > 4) An automatic system (software) will discriminate the invalid
> solutions,
> > e.g., using sorry somewhere, from the valid solutions. After that, it
> will
> > make an ordering according to the running time of each valid solution.
> >
> > 5) Finally, an email with the ranking of his/her solution will be
> > automatically sent to each participant. The participants having ranking
> 1,
> > 2, 3 will receive a prize.
> >
> > When I think about such an international project, I am mainly concerned
> > with people living in economically less developed countries. The idea is
> > that a person from such countries, having the dream of winning an
> > International Olympiad in Isabelle will have a motivation to improve
> > himself/herself in this field. Of course, classification by countries
> > should be avoided and people from highly developed countries should be
> > allowed to participate as well.
> >
> > This is just a dream, I have not enough free time to do something about
> it.
> > My inspiration are the IOI: https://ioinformatics.org/
> >
> > Kind Regards,
> > José M.
> >
> >
>
>
>

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.