[isabelle] International Olympiad in Isabelle?



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.