Email Gateway (Aug 22 2022 at 18:45): Email Gateway (Aug 22 2022 at 18:45):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
max wrote [about the International Olympiad in Isabelle]:
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.
El lun., 18 jun. 2018 a las 8:19, Max Haslbeck (<haslbema@in.tum.de>)
escribió:
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.pdfWe 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,
max2018-06-17 16:04 GMT+02:00 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: Apr 20 2024 at 01:05 UTC