Re: [isabelle] Proving Contests

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 :)


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of José Manuel Rodriguez Caballero <josephcmac at>
Sent: Wednesday, November 7, 2018 4:54:25 PM
To: cl-isabelle-users at
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
the following link):

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:

Kind Regards,
José Manuel Rodriguez Caballero

El mar., 6 nov. 2018 a las 21:26, Gidon Ernst (<gidon.ernst at>)

> 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)
> 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 <
> cl-isabelle-users-bounces at> on behalf of José Manuel
> Rodriguez Caballero <josephcmac at>
> Sent: Wednesday, November 7, 2018 10:59:06 AM
> To: cl-isabelle-users at
> 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:
> Kind Regards,
> José M.

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