Re: [isabelle] International Olympiad in Isabelle?

Dear José,

we had a similar idea for a "proving contest", implemented a prototype
and tested it with the Isabelle group here in Munich.
Simon and I wrote up a few pages documenting the idea:

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.


2018-06-17 16:04 GMT+02:00 José Manuel Rodriguez Caballero <
josephcmac at>:

> 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.

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