[isabelle] International Olympiad in Isabelle?

[José Manuel Rodriguez Caballero]

Hello,
I just want to suggest, as an abstract possibility, that in order to
introduce proof-assistants in popular culture, to organize an International
Olympiad in Isabelle could be a good strategy. I imagine such an Olympiad
as many high school students in a room, in front of their computers, trying
to mechanize the proof of a hard theorem from elementary mathematics that
is written on a blackboard, e.g., a theorem due to Erdos or Ramanujan. To
use papers to write the arguments is forbidden: the proof should go from
their brain to Isabelle in a direct way. The first student who finishes the
proof win (this can be checked in an automatic).

Kind Regards,
José M.

[Makarius]

Post by José Manuel Rodriguez Caballero
I just want to suggest, as an abstract possibility, that in order to
introduce proof-assistants in popular culture, to organize an International
Olympiad in Isabelle could be a good strategy.

Incidentally something like this has happened a few weeks ago at the
national level (of Germany):
https://sketis.net/2018/jugend-forscht-hilbert-meets-isabelle

The Isabelle team even won a special prize by the Federal President of
Germany, Frank-Walter Steinmeier.

There will be a presentation about this (still ongoing) project at the
Isabelle Workshop 2018 at Oxford:
https://easychair.org/smart-program/FLoC2018/Isabelle-2018-07-13.html#talk:71275


Makarius

[José Manuel Rodriguez Caballero]

The technical details aside, I think, the hardest part is to find suitable
tasks (mathematical theorems, riddles, programs + their verification, ...)
that are solvable within - say - 5 hours.

One source of suitable mathematical tasks could be the problems-solutions
section in American Mathematical Monthly (many great mathematician,
including Paul Erdos and Jeffrey Lagarias, contributed with problems and/or
solutions):
https://www.maa.org/press/periodicals/american-mathematical-monthly

Also, a good source of elementary mathematics is The Mathematical Gazzette
(Cambridge): https://www.cambridge.org/core/journals/mathematical-gazette

There is a lot of good elementary mathematics in the collected works of
Pierre de Fermat, Leonhard Euler, James Joseph Sylvester, S. Ramanujan,
Paul Erdos, etc. Finally, my preferred source of non-trivial elementary
mathematics: the Jakob Perelman's books (Algebra can be Fun, Arithmetic for
entertainment, Geometry for Entertainment, Mathematics can be Fun, etc.).

I think that such a "proving contest" should be for highschool students,
because at that age, they have a lot of free time to become wizards in some
specific proof assistant. I remember that, when I was a teenager, I learned
Pascal in high school just to participate in a national contest: that kind
engagement changes teenager lives for good.

José M.

Dear José,
we had a similar idea for a "proving contest", implemented a prototype
version
and tested it with the Isabelle group here in Munich.
http://www21.in.tum.de/~haslbema/documents/provingcontests_draft18.pdf
We are planning to push this further in future.
The technical details aside, I think, the hardest part is to find suitable
tasks (mathematical theorems, riddles, programs + their verification, ...)
that are solvable within - say - 5 hours.
cheers,
max
2018-06-17 16:04 GMT+02:00 José Manuel Rodriguez Caballero <

Post by José Manuel Rodriguez Caballero
Hello,
I just want to suggest, as an abstract possibility, that in order to
introduce proof-assistants in popular culture, to organize an
International
Olympiad in Isabelle could be a good strategy. I imagine such an Olympiad
as many high school students in a room, in front of their computers, trying
to mechanize the proof of a hard theorem from elementary mathematics that
is written on a blackboard, e.g., a theorem due to Erdos or Ramanujan. To
use papers to write the arguments is forbidden: the proof should go from
their brain to Isabelle in a direct way. The first student who finishes the
proof win (this can be checked in an automatic).
Kind Regards,
José M.

[Makarius]

http://www21.in.tum.de/~haslbema/documents/provingcontests_draft18.pdf
We are planning to push this further in future.
The technical details aside ...

An interesting paper.

Note that "the ML level" no longer exists in Isabelle today. You mean
"Isabelle/ML", which is properly integrated into Isabelle/Isar for more
than 10 years. In the past, end-users were accustomed to the Poly/ML
bootstrap environment, which is still available in "isabelle process"
and "isabelle console" today, but rarely used directly in applications.

Moreover note that the brief discussion about the 'sorry' command vs.
checking oracle tags in thm values is unfounded. Neither the Isabelle
documentation nor the implementation supports that claim.

Concerning the general mental model of a bullet-proof checker that can
run unattended and cannot be abused: I don't believe that Isabelle can
ever deliver that. It was not constructed with that idea in mind: after
decades of following a model of benevolent users that don't shoot
themselves in the foot, it is infeasible to do differently in a posthoc
fashion. You need a different proof checker for that, but I don't know a
suitable system.


Makarius

[José Manuel Rodriguez Caballero]

The technical details aside, I think, the hardest part is to find suitable
tasks (mathematical theorems, riddles, programs + their verification, ...)
that are solvable within - say - 5 hours.

Last Friday I solved a mathematical problem from the Putnam Mathematical
Competition and immediately after I formally verified my solution in
Isabelle/HOL. It was nearly 5 hours of work (including solution and formal
verification). I stopped for a coffee and food. So, I think that an
International Olympiad in Isabelle will be possible in such conditions.

The problem was ARITHMETIC PROGRESSIONS in the following link:
https://www.ocf.berkeley.edu/~wwu/riddles/putnam.shtml

My solution is here (it is not the most elegant formalization, because I
was in a hurry trying to be as fast as possible):
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/ArithProgRelPrimes.thy

After the formal verification, my understanding of the problem was much
better than before.

I hope that one day the goals of the so-called Xena Project, i.e.,
mathematical education with proof assistants, will be a current reality in
most of universities of the world:
https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/

Competition is the best way to motivate people to do something new.

Kind Regards,
José M.

Dear José,
we had a similar idea for a "proving contest", implemented a prototype
version
and tested it with the Isabelle group here in Munich.
http://www21.in.tum.de/~haslbema/documents/provingcontests_draft18.pdf
We are planning to push this further in future.
The technical details aside, I think, the hardest part is to find suitable
tasks (mathematical theorems, riddles, programs + their verification, ...)
that are solvable within - say - 5 hours.
cheers,
max
2018-06-17 16:04 GMT+02:00 José Manuel Rodriguez Caballero <

Post by José Manuel Rodriguez Caballero
Hello,
I just want to suggest, as an abstract possibility, that in order to
introduce proof-assistants in popular culture, to organize an
International
Olympiad in Isabelle could be a good strategy. I imagine such an Olympiad
as many high school students in a room, in front of their computers, trying
to mechanize the proof of a hard theorem from elementary mathematics that
is written on a blackboard, e.g., a theorem due to Erdos or Ramanujan. To
use papers to write the arguments is forbidden: the proof should go from
their brain to Isabelle in a direct way. The first student who finishes the
proof win (this can be checked in an automatic).
Kind Regards,
José M.