Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving Contests


view this post on Zulip Email Gateway (Aug 22 2022 at 18:48):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.


Last updated: Apr 20 2024 at 04:19 UTC