Email Gateway (Aug 22 2022 at 17:37): Email Gateway (Aug 22 2022 at 17:37):From: José Manuel Rodriguez Caballero <josephcmac@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.
Last updated: Nov 21 2024 at 12:39 UTC