Re: [isabelle] International Olympiad in Isabelle?



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.
Simon and I wrote up a few pages documenting the idea:
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 <
josephcmac at gmail.com>:

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